代码之家 › 专栏 › 技术社区 › Axel Kemper

SAT解算器与相位节省

sat-solvers z3

Axel Kemper · 技术社区 · 6 年前

DPLL SAT solvers Phase Saving 第一在分支中。

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

结果运行时间如下所示:

这可能只是(坏)运气,但差别非常大。这是一个特别的惊喜 超小卫星 以我为例,它的性能超过了所有的现代解算器。

我的问题是:

对这些差异有什么解释吗?
极性和相位节省的最佳实践?

1 回复 | 直到 5 年前

Kyle Jones 6 年前

从你的测试中不能得出结论。DPLL和基于它的解算器根据初始搜索条件表现出重尾行为。这意味着同一个解算器在同一个实例上可以有短运行时间和长运行时间,具体取决于随机重启发生的时间等因素。不同解算器之间的搜索时间可能会有很大差异,这取决于(例如)它们如何选择决策变量,即使没有阶段保存和随机重新启动带来的额外复杂性。

推荐文章