2
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • 2
    $\begingroup$ Rather than using "EDIT:", we'd prefer that you revise your question to read well for someone who encounters it for the first time. See cs.meta.stackexchange.com/q/657/755. No need to mark what has changed - we have built-in revision history. $\endgroup$
    – D.W. ♦
    Mar 22, 2020 at 1:56

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
19
  • $\begingroup$ Thank you for your answer. However, not every Boolean function over $n$ variables can be expressed as a Boolean formula of length polynomial to $n$. Then, for all Boolean function whose minimal formula has length exponential to the number of variables, and even if we convert them to 3SAT using Tseytin transformation, the resulting 3SAT formula, though polynomial to the minimal formula, will still be exponential to the number of variables? $\endgroup$
    – Hui Wang
    Mar 22, 2020 at 0:55
  • 1
    $\begingroup$ @HuiWang, see edited answer for further explanation of the chain of reasoning. $\endgroup$
    – D.W. ♦
    Mar 22, 2020 at 0:59
  • 2
    $\begingroup$ @HuiWang, I am aware of that, but I'm not seeing how it is relevant. The SAT problem is about CNF formulas, not arbitrary Boolean functions. This platform is not made for interactive discussions. if you have a follow-up question, I suggest asking it using the 'Ask Question' button in the upper-right, and provide full context. $\endgroup$
    – D.W. ♦
    Mar 22, 2020 at 1:38
  • 1
    $\begingroup$ @HuiWang, sure, but that's beside the point (it is not relevant to the points I am making, and it does not contradict or invalidate anything I wrote). The chain of reasoning I present is valid despite that fact. I suggest making sure you understand each step of the sequence of implications that I describe. Perhaps read the last paragraph of my answer again. I suggest trying to work out a plausible scenario that you think is internally consistent, that specifies which satisfiability problems can be solved in polynomial time (3CNFs? CNFs? Boolean formulas?) and which can't. $\endgroup$
    – D.W. ♦
    Mar 22, 2020 at 2:30
  • 1
    $\begingroup$ @HuiWang, those competitions don't involve worst-case inputs. If you want to know "what is the evidence that the worst-case running time of current SAT solvers is not polynomial in the length of the CNF?", I suggest asking that separately using the 'Ask Question' button. This platform is not designed for interactive discussions or extended back-and-forths. $\endgroup$
    – D.W. ♦
    Mar 23, 2020 at 1:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.