SAT 求解：DPLL 与？答案

【问题标题】：SAT-Solving: DPLL vs.?SAT 求解：DPLL 与？
【发布时间】：2015-08-22 04:07:31
【问题描述】：

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

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

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

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

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

感谢您的帮助。

【问题讨论】：

【解决方案1】：

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

【讨论】：

【解决方案2】：

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

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

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

【讨论】：