random - SAT 求解：DPLL 与？

Question

现在我正在写关于解决 SAT 的文章，但我被困在了一个点上。我希望你能帮助我。

我想描述一些解决 SAT 问题的方法。现在我有三种不同的方法：

1. 蛮力
2. 随机（天真）
3. DPLL（具有不同的启发式）
4. ? 失踪 ？
5. ...

我的问题是唯一有效的算法是 DPLL（以及其他一些与 DPLL 略有不同的算法）。因此我没有什么可以比较 DPLL 的。

我的问题：如果您能告诉我一些不基于 DPLL (DP) 的算法，我可以将其与之进行比较，那就太好了。

以下是我发现的一些，但无法确定它们是否是一个不错的选择，或者是否有更好的选择：

• 莫尼恩-斯佩肯迈尔
• Dantsin、Goerdt、Hirsch 和 Schöning
• Paturi-Pudlák-Zane-算法
• 霍夫迈斯特、舍宁、舒勒和渡边

谢谢你的帮助。

Answer 1

最先进的卫星求解器目前使用基于 DPLL 的 CDCL（冲突驱动子句学习）。

Answer 2

在您建议的 SAT 求解算法中，bruteforce 和 DPLL 都是完整的算法，只要有足够的时间，就可以保证找到令人满意的任务或证明问题不可满足。正如 Million 所提到的，CDCL 是 DPLL 的一个进步，也已经完成。

如果您想讨论替代方案，我建议您查看不完整算法。这些通常基于随机本地搜索，包括 GSAT 和 WalkSAT。虽然这些算法不能保证找到答案，但它们传统上非常擅长解决随机（相对于工业）SAT 问题。它们还被用于解决比任何实现基于 DPLL 的算法的求解器都能够解决的更大的 SAT 问题。

对于进一步的研究，我推荐 Biere 的精彩著作《可满足性手册》。