SAT求解器在代数攻击（例如walksat和minisat）中非常重要。

但是，在解决此处可用的基准问题时，两者之间存在巨大的性能差异-Walksat的速度比minisat快得多问题。为什么会这样？

这种walksat的实现似乎在性能上有所改进-是否有任何理由未将其纳入国际SAT竞赛？

评论

这将更适合CSTheory SE。我认为这是Crypto的主题，但您肯定会在那得到更好的答复。

#1 楼

Walksat是一个不完整的求解器。这意味着它试图找到许多迭代的解决方案。如果确实找到了解决方案，则回答该解决方案，否则回答“不知道”。 Walksat使用一种随机游走的形式来搜索启发式解决方案以指导其发展。另一方面，Minisat拥有足够的计算资源，可以为您提供解决方案或答案，该问题是无法满足的（并且通过添加证明跟踪，您还将获得证明）。 Minsat使用了现代形式的DPLL。

对于您的问题的简短回答是，找到答案（如果存在）要比证明没有答案要容易。

较长的答案是，walksat仅比minisat快，如果有很多解决方案，并且它们的结构在搜索空间中属于特殊类型。

在带有基准的页面上我找不到任何关于walksat的参考。您是否自己在一些基准测试中走过了路？您是否在已知无法满足的基准测试过walksat？

评论

$ \ begingroup $
回答“您自己是否在某些基准测试中走过睾丸？”是。并回答“您是否在已知无法满足的基准测试了walksat？”没有。
$ \ endgroup $
–ir01
2011年8月3日在10:39


#2 楼

SAT求解器没有单一的方法-并非每种方法都对每个问题都同样有效。在给定问题上表现出色的SAT求解器通常不一定能很好地工作。

典型地，SAT求解器会采用一整套技巧-决定采用哪种启发式方法是求解器之间的最大差异之一。不同的启发式方法可以很好地解决不同类型的问题，求解器必须确定当前问题的特征，以决定使用哪种启发式方法（除非用户指定要使用哪种启发式方法，如果一个人知道该怎么做，或者可以进行实验）目的）。

关于为什么某个给定的求解器未参加国际SAT竞赛的原因，您必须询问求解器的创建者！我很确定如果他们愿意...他们可以提交它。