线性饱和-不饱和与线性不饱和饱和

Question

我知道以上两种算法都需要迭代求解才能找到MAXSAT问题的最优解，但我想知道为什么从可满足的一侧开始，同时为MAXSAT找到解决方案比从不可满足的侧搜索更好？

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

Answer 1

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

因此，有一种方法，你从简单的例子开始，这些例子逐渐变得更难写SAT/USAT证明，而另一种方法则从尝试写硬证明开始，并在下一次迭代中不得不写一个更难的证明。