Time complexities of state-of-the-art SAT solvers with respect to length of the formula

Question

I am learning about DPLL and CDCL SAT solvers, and I know that they have time complexity exponential to the number of variables.

If I am not mistaken, one of the reasons why most believe P does not equal to NP is that there exists no polynomial-time algorithm for SAT despite tremendous effort from mathematicians and computer scientists. However, the P vs NP problem only cares about the time complexity with respect to the length of the formula, not the number of variables.

If these state-of-the-art SAT solvers were run on 3CNF formulas, then a time complexity exponential to the number of variables implies a time complexity exponential to the length of the 3CNF.

However, if they were run on arbitrary CNFs, whose length can be exponential to the number of variables, then a time complexity exponential to the number of variables would not necessarily imply a time complexity exponential to the length of the CNF.

Thus, a related question is, are these SAT solvers run on 3CNF or CNF while measuring time complexity?

Answer 1

For 3SAT, the number of variables is polynomially related to the number of clauses. (See the end for the justification.)

Consequently, any algorithm for 3SAT whose running time is polynomial in the number of clauses would also be polynomial in the number of variables; and any algorithm for 3SAT whose running time is polynomial in the number of variables would also be polynomial in the number of clauses.

It is known that there is a polynomial-time algorithm for 3SAT, if and only if there is a polynomial-time algorithm for SAT, if and only if there is a polynomial-time algorithm for CircuitSAT (e.g., for formulas). Also, despite decades of work on SAT solvers, no one knows any algorithm for 3SAT that runs in polynomial time (or indeed in less than exponential time in the worst case). You could take this as evidence that there is no polynomial-time algorithm for 3SAT; which implies that there is no polynomial-time algorithm for SAT or CircuitSAT, either, and also implies that P != NP.

---

Justification: Let $n$ denote the number of variables and $m$ the number of clauses. We have $n \le 3m$ (a variable that doesn't appear in any clause can be ignored) and $m \le 8n^3$ (each clause has three literals, and you can ignore repeated clauses). It follows that $n/3 \le m \le 8n^3$ and $\sqrt[3]{m/8} \le n \le 3m$, i.e., each is polynomially related to the other.

---

I see that you revised your question. That clarifies that I think you have a misconception. You talk about "run[ning] [a SAT solver] on arbitrary Boolean formulas". However, you can't run a SAT solver on an arbitrary Boolean formula. SAT solvers only work on CNF formulas.

However, we do know that any Boolean formula can be converted to an equisatisfiable CNF formula of size at most polynomial in the size of the formula, and vice versa. If you had an algorithm that could test satisfiability of arbitrary Boolean formulas in time polynomial in the size of the formula, then it would follow that you have an algorithm that could test satisfiability of 3CNF formulas in time polynomial in the size of the formula (every 3CNF formula is a Boolean formula), and thus an algorithm that could test satisfiability of 3CNF formulas in time polynomial in the number of variables -- which contradicts the available evidence. So, if you believe that there is no algorithm to solve 3SAT in time polynomial in the number of variables, then you should also believe that there is no algorithm to test satisfiability of arbitrary Boolean formulas in time polynomial in the size of the formula.