I know that there is no algorithm for converting any logical formula to DNF so even though we have an efficient algorithm to solve DNFSAT we can't solve formulaSAT in deterministic polynomial time. But what makes the finding of an efficient CNF algorithm solve formulaSAT in polynomial time? Because I'm guessing that the complexity of converting a logical formula to a DNF would be the same as the complexity of converting a formula to CNF so even if we find an efficient algorithm for CNFSAT we won't be able to convert any formula into CNF and therefore we can't solve formulaSAT also! Or am I wrong and the problem of formulaSAT is not in NP?! An example of what I mean by a formula: (¬A∨B)∧¬((A∧¬C∧(B∨D))∨(C∧D))

  • $\begingroup$ There is an algorithm to convert an arbitrary formula to DNF. It just takes exponential time. $\endgroup$ – Yuval Filmus Mar 8 at 7:04
  • $\begingroup$ Yeah I know! I meant that there is no efficient algorithm to convert an arbitrary formula to a DNF formula. @YuvalFilmus $\endgroup$ – Roofnos Mar 10 at 23:13

When converting an arbitrary formula into a CNF, you are introducing extension variables. These are new variables that represent subformulas of your formula.

Let us take the following simple formula as an example:

$$ A \lor (B \land C). $$

In order to convert this into a CNF, we need to replace $B \land C$ with an extension variable $\alpha$ which has the same truth value of $B \land C$. We can easily express "$\alpha = B \land C$" as a CNF (or as a DNF). After replacing $B \land C$ with $\alpha$, we obtain the formula $$ (A \lor \alpha) \land \text{"$\alpha = B \land C$"}. $$ (You need to replace "$\alpha = B \land C$" with a CNF.) This formula is equisatisfiable with the original formula: the original formula is satisfiable iff the new formula is satisfiable. Therefore if we are interested in knowing whether the original formula is satisfiable, we can instead ask whether the new one is.

In the transformation outlined above, we used the fact that the class of CNFs is closed under conjunction. That is, we could express add the condition "$\alpha = B \land C$" to our formula while retaining its CNF form. The same is not the case for DNFs, which are closed under disjunction but not under conjunction.

Indeed, consider the opposite situation, in which we want to convert $A \land (B \lor C)$ into an equisatisfiable DNF. We can easily express $\alpha = B \lor C$ as a DNF; the problem is that $(A \land \alpha) \land \text{"$\alpha = B \lor C$"}$ is not a DNF, since we joined $A \land \alpha$ and $\alpha = B \lor C$ with the wrong connective.

  • $\begingroup$ Do you mean by (A∨α)∧"α=B∧C" the formula (A∨α)∧(α↔(B∧C))? I got this but what about higher formulas?! We can judge that a subformula is satisfiable but when we go higher we lose information about variables and the same variable that was a part of the subformula you decide its satisfiability could appear again in a higher clause so even if you know the satisfiability of the subformula it won't help you. Because if it was that easy then we can begin from inside clauses and go higher since we know that this is easy! the formula you gave becomes unsatisfiable if it is a subformula within ¬A∧¬α∧β. $\endgroup$ – Roofnos Mar 10 at 23:09
  • $\begingroup$ The same idea works in general. Just use a fresh extension variable each time. It’s a nice exercise to work it out. $\endgroup$ – Yuval Filmus Mar 10 at 23:11
  • $\begingroup$ More generally, CNF-SAT is NP-complete. $\endgroup$ – Yuval Filmus Mar 10 at 23:18
  • $\begingroup$ I've read about Tseitin transformation this morning and I know now how the polynomial algorithm works. Did you mean the same method or another method? Because sadly I can't get it from a small example !! $\endgroup$ – Roofnos Mar 10 at 23:19
  • $\begingroup$ It’s exactly the same method. $\endgroup$ – Yuval Filmus Mar 10 at 23:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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