让我谈谈一般的优化，而不是仅仅谈论 SAT 求解器。许多经济问题可以被视为优化问题：例如，FedEx 可能有一个包裹清单和这些包裹的目的地，并且必须决定哪些包裹放在哪些卡车上，以及以什么顺序交付这些包裹。

如果你写出这个问题的数学描述，就会有大量可能的解决方案，以及一种明确的方法来评估两个解决方案中的哪一个更好。求解器是一种算法，它将评估一个解决方案，提出另一个解决方案，然后评估那个解决方案，依此类推。

在小案例和简单问题中，求解器也可以通过证明它实际上是可能的最佳解决方案来终止。但通常情况下，求解器只会报告“这是我见过的最好的解决方案”，并且会被使用。求解器的改进意味着您可以可靠地获得比以前更低成本的解决方案。

对于 SAT 问题，SAT 上的维基百科页面给出了一些示例：

由于 SAT 问题是 NP 完全问题，因此只有具有指数最坏情况复杂度的算法才为人所知。尽管如此，SAT 的高效和可扩展算法在过去十年[何时？] 中被开发出来，并为我们自动解决涉及数万个变量和数百万个约束（即子句）的问题实例的能力做出了巨大的进步。 [1] 电子设计自动化 (EDA) 中此类问题的示例包括形式等效检查、模型检查、流水线微处理器的形式验证、[12] 自动测试模式生成、FPGA 路由、[14] 规划和调度问题等。SAT 求解引擎现在被认为是 EDA 工具箱中的重要组件。

SAT 求解器的一个实际示例是在 python conda 包管理器中找到一组兼容的包版本。

（例如，参见https://www.anaconda.com/blog/understanding-and-improving-condas-performance）

SAT求解器的实际应用也包括（见http://www.carstensinz.de/talks/RISC-2005.pdf）：

• 产品配置
• 硬件验证
• 有界模型检查
• （硬件）等价检查
• 异步电路合成 (IBM)
• 软件验证
• 专家系统验证
• 规划（空中交通管制、电报路由）
• 日程安排（体育比赛）
• 有限数学（拟群）
• 密码分析