与DPLL相比，CDCL的运行时间

Question

与DPLL求解器相比，以冲突驱动的子句学习SAT求解器的复杂性是什么？是否证明CDCL通常更快？是否有SAT的实例很难CDCL，但对于DPLL来说很容易？

Answer 1

在最坏情况下，CDCL和DPLL都需要指数时间。我不确定是否可以证明CDCL总是比每个实例的DPLL都快，但是 重大的 经验数据表明其主导。有关精美的简短概述，请参阅演示文稿 布尔值满意度解决：过去，现在和未来 Joao Marques-Silva。他在网上也有很多相关的谈话，请参阅 这里.

CDCL是 这 在所有现代求解器中主导求解器。我会声称CDCL确实确实占主导地位，这是因为它基本上是一个基于DPLL的程序，但具有其他增强功能。它使用在搜索过程中获得的信息，重新启动策略，特殊数据结构等。

在某些实例中，所有已知的DPLL样算法都以指数时间运行。例如，Alekhnovich等。 [1]展示了这样一个3个SAT实例的家庭。有关可满足感的更多信息，理论和实用性，我认为最好的来源之一是 满意度手册 2]和常规 国际理论和可满足性测试的应用会议, ，被称为坐着。

---

1] Alekhnovich，M.，Hirsch，E。和Itykson，D。DPLL算法在可满足公式上的运行时间的指数下限。 Jar，35（1-3），51-72，2005。

2] Biere，A.，Heule，M.，Van Maaren，H。和Walsh，T。（编辑）。满意度手册。 iOS出版社，2009年。