constraint-programming - 线性饱和未饱和与线性未饱和饱和

Question

我知道上述两种算法都属于迭代解决方案以找到 MAXSAT 问题的最佳解决方案，但我想知道为什么从可满足方面开始同时为 MAXSAT 找到解决方案比从不可满足方面搜索更好？

同样在这里，可满足方面意味着放宽所有可能的软条款，直到我们达到 UNSAT 和不可满足方面意味着从不放宽条款开始增加数量，直到我们达到 SAT

Answer 1

MAX-SAT 问题通常与不可满足的公式有关。在一般情况下，不可满足性证明比可满足性证明更难编写。当您从实例中删除约束时，不可满足性证明也往往会变得更加困难，过度约束是一些不可满足的实例很容易的主要原因。

因此，使用一种方法，您从简单的实例开始，逐渐变得更难为其编写 SAT/UNSAT 证明，而另一种方法则开始尝试编写硬证明，并通过在下一次迭代中编写更难的证明来获得回报。