最先进的 SAT 求解器的时间复杂度与公式长度的关系

Question

我正在学习 DPLL 和 CDCL SAT 求解器，并且我知道它们的时间复杂度与变量数量成指数关系。

如果我没记错的话，大多数人认为 P 不等于 NP 的原因之一是，尽管数学家和计算机科学家付出了巨大的努力，但 SAT 并不存在多项式时间算法。然而，P vs NP 问题只关心相对于公式长度的时间复杂度，而不关心变量的数量。

如果这些最先进的 SAT 求解器在 3CNF 公式上运行，那么时间复杂度与变量数量呈指数关系意味着时间复杂度与 3CNF 长度呈指数关系。

然而，如果它们在任意 CNF 上运行，其长度可以与变量数量呈指数关系，那么与变量数量呈指数关系的时间复杂度不一定意味着与 CNF 长度呈指数关系的时间复杂度。

因此，一个相关的问题是，这些 SAT 求解器在测量时间复杂度时是在 3CNF 还是 CNF 上运行？

Answer 1

对于 3SAT，变量的数量与子句的数量呈多项式相关。（理由见文末。）

因此，任何运行时间是子句数量多项式的 3SAT 算法也将是变量数量的多项式；任何运行时间是变量数量多项式的 3SAT 算法也将是子句数量的多项式。

众所周知，当且仅当存在 SAT 的多项式时间算法时，当且仅当存在 SAT 的多项式时间算法时，当且仅当存在 CircuitSAT 的多项式时间算法（例如，对于公式）时，存在 3SAT 的多项式时间算法。此外，尽管对 SAT 求解器进行了数十年的研究，但没有人知道任何在多项式时间内运行（或者在最坏情况下小于指数时间）的 3SAT 算法。你可以以此作为证据，证明 3SAT 没有多项式时间算法；这意味着 SAT 或 CircuitSAT 也没有多项式时间算法，并且还意味着 P != NP。

---

理由：让 $n$ 表示变量的数量， $百万$ 子句的数量。我们有 $n \le 3m$ （没有出现在任何子句中的变量可以被忽略）和 $m \le 8n^3$ （每个子句有三个文字，您可以忽略重复的子句）。它遵循 $n/3 \le m \le 8n^3$ 和 $\sqrt[3]{m/8} \le n \le 3m$, ，即每个都与另一个多项式相关。

---

我看到你修改了你的问题。这澄清了我认为你有一个误解。您谈论“在任意布尔公式上运行[ning] [SAT 求解器]”。但是，您无法对任意布尔公式运行 SAT 求解器。SAT 求解器仅适用于 CNF 公式。

然而，我们确实知道任何布尔公式都可以转换为可等满足的 CNF 公式，其大小最多为公式大小的多项式，反之亦然。如果您有一个算法可以在公式大小的时间多项式中测试任意布尔公式的可满足性，那么您就有一个可以在公式大小的时间多项式中测试 3CNF 公式的可满足性的算法（每个3CNF 公式是一个布尔公式），因此是一种可以测试 3CNF 公式在变量数量的时间多项式中的可满足性的算法 - 这与现有证据相矛盾。因此，如果您认为没有算法可以解决变量数量的时间多项式中的 3SAT，那么您也应该相信没有算法可以测试公式大小的时间多项式中的任意布尔公式的可满足性。