线性卫星与线性非卫星

Question

我知道上述两种算法都采用迭代解法来寻找MAXSAT问题的最优解，但我想知道为什么从可满足的方面开始，同时为MAXSAT找到一个解决方案，要比从不可满足的方面寻找它更好呢？

在这里，可满足的一面意味着在我们到达UNSAT之前放松所有可能的软子句，而不可满足方则意味着从没有子句开始，直到我们到达SAT才能增加数量。

Answer 1

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

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