z3 - SAT 求解器和相位节省

Question

DPLL SAT 求解器通常应用Phase Saving启发式算法。这个想法是记住每个变量的最后一次赋值并在分支中 首先使用它。

为了试验分支极性和相位节省的效果，我尝试了几个 SAT 求解器并修改了相位设置。都是Windows 64 位端口，以单线程模式运行。我总是使用中等复杂度的相同示例输入（5619 个变量，11261 个子句，在解决方案中，所有变量的 4% 为真，96% 为假）。

下面列出了生成的运行时间：

这可能只是（坏）运气，但差异非常大。在我的例子中， MiniSat的表现优于所有现代求解器，这让我感到特别惊讶。

我的问题：

对这些差异有任何解释吗？
极性和相位节省的最佳实践？

标签： z3sat-solversdpll

Answer 1

从您的测试中无法得出任何结论。众所周知，DPLL 和基于它的求解器会根据初始搜索条件表现出重尾行为。这意味着同一个求解器可以在同一个实例上同时具有短运行时和长运行时间，具体取决于随机重启发生的时间等因素。不同求解器的搜索时间可能会有很大差异，这取决于（例如）他们如何选择决策变量，即使没有增加相位保存和随机重启的复杂性。