logicsatisfiabilitycnf

SAT can be verified in polynomial time, by a conversion to CNF, then verifying the SAT of the CNF in polynomial. What is wrong with this argument?


we know that any expression can be converted to a CNF in linear time where the CNF result is not 'logically equivalent' to the original expression but the 'satisfiability' is invariant meaning that the CNF is satisfiable if and only if the original expression is satisfiable (this can be done for example by calculating the 'Tseitin derivative'). Given that the satisfiability of the CNF can be checked in polynomial time, then the satisfiability of the original expression can be checked in polynomial time. Therefore, the satisfiability of any expression can be checked in polynomial time. However, the SAT problem is NP-complete so this is not true. But where am I going wrong here? I assume that the explanation comes from "CNF is not logically equivalent to the original expression" but then again this is not important in checking the satisfiability (?). Thank you in advance for any help.


Solution

  • So the confusion here was that the satisfiability of DNFs (disjunctive normal forms) can be solved in polynomial time - we just check all of the disjunct and if there is a disjunct which does not include any complementary literals then it is satisfiable. We can solve the validity of CNFs (conjunctive normal forms) in polynomial time as well - because it is valid if all of the conjuncts contain complementary literals. But we the problem of validity of DNFs or satisfiability of CNFs is NP-complete. Note that any logical expression in a CNF form which complemented will be in DNF form so it is rational to think that the validity of a CNF is equivalent to the unsatisfiability of its complement (which is in turn a DNF). I got the answer a month ago but forgot to share it with you. Hope this helps anyone who encountered the same confusion as me.