0
$\begingroup$

I am confused about the hardness of SAT(Boolean Satisfiability Problem). It takes polynomial time to transform any given boolean formula $f$ to a conjunctive normal form. I mean polynomial in the length of the formula. Then we can easily jugde if $f$ is always true by checking if the conjunctive normal form covers all expressions like $x_1 \neg x_2 \dots x_n$.

The whole algorithm is polynomial in the length of $f$.

When people say SAT is hard, do they mean that we can not find algorithms to solve SAT that are polynomial in the number of variables?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

It is not true that any Boolen $f$ can be transformed into conjunctive normal form in polynomial time. Consider $$f = (x_1 \land y_1) \lor (x_2 \land y_2) \lor \ldots \lor (x_n \land y_n).$$ That is, $f$ has $2n$ variables and $n$ (disjunctive) clauses (let us say the length of $f$ is the number of symbols including parantheses), then its length is $6n-1$ Then $f$ in CNF is $$f \equiv (x_1 \lor x_2 \lor \ldots \lor x_n) \land (y_1 \lor x_2 \ldots \lor x_n) \land (x_1 \lor y_2 \lor \ldots \lor x_n) \land \ldots \land (y_1 \lor y_2 \lor \ldots \lor x_n) \land (y_1 \lor y_2 \lor \ldots \lor y_n),$$ which has $2^n$ clauses and length $2^n (2n+2)$, i.e. exponential in the length of $f$.

About the second statement

checking all expressions like $x_1 \neg x_2 \ldots x_n$

I do not quite get what you mean by that but whatever it is it seems to be exponential in $n$ as well.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ Any boolean formula $f$ can be converted to an equi-satisfiable boolean formula $f'$ which is linear in the size of the original formula (and takes linear time). Here, equi-satisfiable means that $f'$ is satisfiable iff $f$ is satisfiable. This is done using the Tseytin transformation technique. SAT solvers use this to convert formulas into CNF. But yes, even though conversion to CNF can be done in P, solving is still exponential. $\endgroup$
    – sherlock
    Commented Oct 30 at 0:24
  • $\begingroup$ This is definitely interesting and important additional context. For the decision problem whether an arbitrary Boolean formula is satisfiable, it suffices to check any equi-satisfiable formula. If you are, however, interested in a satisfying assignment for the original formula, you might not get the desired result using Tseitin's transformation. $\endgroup$
    – ttnick
    Commented Oct 30 at 16:43
  • 1
    $\begingroup$ No, you can get the satisfying assignment for the original formula while using the Tseitin's transformation. The transformation adds some auxiliary variables and keeps the original variables as is. Once you get a satisfying assignment for the transformed formula, you can just drop the valuations of the auxiliary variables to get the satisfying assignment for the original formula. SAT solvers do use this to get the model when get-model is invoked. $\endgroup$
    – sherlock
    Commented Oct 30 at 20:48

Your Answer

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

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