SAT 求解器和相位节省答案

【问题标题】：SAT Solvers and Phase SavingSAT 求解器和相位节省
【发布时间】：2018-10-28 12:12:51
【问题描述】：

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

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

生成的运行时间如下所示：

这可能只是（坏）运气，但差异非常大。在我的示例中，MiniSat 优于所有现代求解器，这是一个特别的惊喜。

我的问题：

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

【问题讨论】：

标签： z3 sat-solvers dpll

【解决方案1】：

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

【讨论】：