optimization - SAT和线性规划有什么区别

Question

我有一个受线性约束的优化问题。
如何知道哪种方法更适合建模和解决问题。
我通常会询问将问题作为可满足性问题(SAT 或 SMT)解决与作为线性规划问题(ILP 或 MILP)解决。

我对这两方面的知识都不多。因此，如果您有任何答案，请简化您的答案。

Answer 1

一般来说，区别在于SAT只尝试可行的解决方案，而ILP则试图优化受约束的东西。我相信一些 ILP 求解器实际上使用 SAT 求解器来获得初始可行解。您在评论中描述的传感器阵列问题被表述为 ILP:“最小化这个主题。” SAT 版本会选择可接受的最大传感器数量并将其用作约束。现在，这是一个可满足性问题，但不是很容易用合取范式表达的问题。我建议使用具有整数理论的求解器。我最喜欢的是Z3。

然而，在你放弃优化之前，你应该尝试 GMPL/GLPK。您可能会惊讶于您的问题是多么容易处理。如果你不那么幸运，把它变成一个可满足性问题并带出Z3。