2
$\begingroup$

I have been reading up on Boolean logic and, specifically, the Boolean satisfiability problem. I have seen several people mention that the expression must be converted to conjunctive normal form (CNF) before it can be solved. Why is this the case?

I understand that propositional formulae would be quite "chaotic" if not in a standard form, but why specifically CNF? Or, more specifically, has CNF been proven to be the best form to solve in? Or, has a better form merely not been found? It is possible there is a better form left undiscovered?

$\endgroup$
1
$\begingroup$

We like conjunctive normal form because all circuits can be transformed into conjunctive normal from in linear time via the Tseitin Transformation. It's a clean, normalized data structure for solver implementation. CNF conversion without Tseitin variables may lead to exponential expansion.

That's the standard answer, but, as you see, there are nuances. Firstly, does the Tseitin transform introduce unnecessary complexity into the solving process? Secondly, why does conjunctive normal form not dualize to disjunctive normal form if the two are related only by negation? Thirdly, are we discarding important information from this one-way conversion of circuit to conjunctive normal form?

If the worst-case complexity of the solver is exponential as conjectured by $P \neq NP$, then one might anticipate the Tseitin transformation to drastically reduce solver efficiency.

Consider a formula $F$ defined by a circuit with $n$ inputs and $m$ internal gates. The circuit's boolean outcome is determined uniquely from assignments to the $n$ inputs, but, after the conversion, the CNF instance contains $n + m$ variables. The space of possible decision branches has been transformed from $2^n$ to $2^{n+m}$.

An astute person would recognize that not all $2^{n+m}$ decision branches are interesting for the solver. For any assignment of the original set of $n$ variables, the additional $m$ Tseitin variables are uniquely determined. In practice, a boolean satisfiability solver handles the added complexity of Tseitin variables by trivial unit propagation, a linear operation to the instance's matrix complexity. So, at least from a practical perspective, applying conjunctive normal form transformations does not change the runtime complexity of satisfiability procedures. You can even apply the Tseitin transform in multiple iterations - beginning with a formula, converting to conjunctive normal form, taking that to be a new formula, converting to conjunctive normal from again, etc. - and the impact on runtime complexity is negligible. Conflict-driven clause learning procedures are very good at zeroing-in on the problems fundamental constraints as opposed to definitional complexity.

Secondly, the relation of CNF and DNF normal forms arise from quantification. If $F$ is some formula and $T$ is some other formula not containing $x$ (Tseitin subformula), consider the instance that binds $x$ to the result of $T$:

$$(\exists \dots)\ \exists x\text{ st. } F \land (x \leftrightarrow T)$$

Assume that all the variables other than $x$ are given assignments, then consider cases for $x$. If $x$ is assigned to be inconsistent with $T$, then the conjunction fails and the entire instance is unsatisfiable. Otherwise, the right side of the conjunction is always satisfied and $x$ agrees with $T$. For the instance to be true, $x$ must be consistent with $T$.

You can define a dual transform over DNF and universal variables like so.

$$(\forall \dots)\ \forall x\text{ st. } F \lor !(x \leftrightarrow T)$$

Similar logic applies for universal quantification: if $x$ is inconsistent with $T$, then the right hand side dominates and the formula is trivially satisfiable. Otherwise, $x$ is bound to $T$ over $F$. Again, for the instance to be (universally) true, $x$ must be consistent with $T$ within $F$.

As far as Tseitin variables are concerned, existential quantification is inextricably bound to conjunction and universal quantification likewise to disjunction. Since SAT solvers only use existential quantification, such a construction is only possible to do in CNF.

QBF solvers use both universal and existential quantification, so the distinction between normal forms for them is less rigid. Any QBF circuit can be transformed to CNF, DNF, or a mixed combination of the two, depending on the quantifications you choose for the Tseitin variables. In QBF solving, there is an alternative standard problem format, called QCIR, that maintains the original formulaic structure. See: Non-CNF QBF Solving with QCIR

Last but not least, is there extra information relevant to the instance that isn't sufficiently captured by CNF? The answer to this is probably yes. If we consider resolution as a standard proof procedure for unsatisfiable SAT outcomes, then there exist counterexamples - namely the pigeonhole problem - where the size of the proof scales exponentially. Tseitin introduced a new system called "extended resolution" that nullified the exponential proof argument on the pigeonhole problem.

The basic idea behind extended resolution is to add extra constraints to the CNF, $x \leftrightarrow a \lor b$. These constraints are effectively just new Tseitin variables, except they eliminate exponential blowup in the resolution proofs instead of CNF conversion of the original circuit. It is unknown whether extended resolution admits polynomial-size proofs of unsatisfiability in general. That would show $\text{NP} = \text{co-NP}$. I mention it because the extra constraints added by extended resolution could be considered to be a stronger form of CNF.

Edit: I should also add, on the last point, that resolution proofs in SAT are inextricably bound to CNF in the unsatisfiable case. Each branch of a resolution proof is a CNF clause, or subset thereof, of the original problem instance. DRAT, the proof standard of real SAT solvers, also operates closely on the CNF form. In the satisfiable case, you can interpret the set of variable assignments as being a singular DNF clause. That is to say, these clausal normal forms are relevant not just to circuit specification, but also to the verifiable justifications for the positive and negative solver outcomes.

$\endgroup$
8
  • $\begingroup$ Wow! This is extremely dense, and I had to read over it a few times to fully grasp what you're saying. Thank you for this! However, I'm still a bit lost on why stay with CNF (if our goal is efficiency). It works, I can see that, and there's a lot of math behind it. However, I am unsure if what you've said here disproves the existence of another form that is both easily converted to and more efficient to solve than CNF (which is my main question). If such a form exists, I feel it would be wise for us to use it. $\endgroup$ Oct 6 at 15:38
  • $\begingroup$ @user3670473 Do you have a different normal form in mind that isn't trivially transformable to CNF? There are some bounds on solver complexity for circuit fan-in here: cstheory.stackexchange.com/questions/93/… $\endgroup$ Oct 6 at 15:47
  • $\begingroup$ But nothing has been proven (or disproven) of the nature that you describe. $\endgroup$ Oct 6 at 15:49
  • $\begingroup$ I'm exploring possibilities myself, but I have not yet landed on a rigorously defined form and solution method. I just thought I would ask here if it were a lost cause or not. I'll take a look at that link to inform me in my exploration. $\endgroup$ Oct 6 at 15:52
  • 1
    $\begingroup$ What you're looking to do sounds like a contrived reformulation of P=NP and is unlikely to be fruitful. Check out this video on N J Wildberger where he does something similar. youtube.com/watch?v=Gz89q6L99Kg The form he uses is called "algebraic normal form". The catch is that it does not have an efficient encoding procedure of the nature of the Tseitin transform on CNF. $\endgroup$ Oct 6 at 16:03
6
$\begingroup$

Conjunctive normal form first appears, in this context, in Davis and Putnam's A computing procedure for quantification theory, in which they describe a primitive form of the DPLL algorithm (which appears in a follow-up work of Davis, Logemann, and Loveland, and is the basis of all modern SAT solvers). They explain that one key property of CNF is that any formula can be efficiently converted to an equi-satisfiable CNF, which does not appear to be the case for DNFs, for example; so assuming that the formula is in CNF is "without loss of generality". The DPLL algorithm could in principle work on more general CSPs (conjunctions of arbitrary constraints), though I'm not sure that the important modern technique of clause learning generalizes to this setting.

Cook's The complexity of theorem-proving procedures proves the NP-completeness of SAT and 3SAT, which indicates that satisfiable of CNFs, and even 3CNFs, is a "hardest" problem, and a good candidate for a problem not solvable in polynomial time. As shown in Karp's Reducibility among combinatorial problems, and in more modern work on fine-grained complexity, it is also a good starting point for NP-hardness reductions.

Is CNF the "best" representation? This depends on what problem you're trying to solve. If you're trying to solve linear equations, then representing the problem as a set of linear equations is far superior. SMT solvers, heavily used in verification, also use a richer representation. Sometimes an integer program is the best way to formulate a problem. Nevertheless, the ubiquity of SAT solvers shows that in practice, CNF is often a highly useful normal form from a practical point of view.

$\endgroup$
5
  • $\begingroup$ Thanks for this info! I guess to re-iterate one of my questions: is it possible that there emains an undiscovered form that has all the advantages of CNF, but also includes more advantages, making it better for general SAT problems? $\endgroup$ Oct 4 at 16:14
  • $\begingroup$ In some sense, the answer is negative, since SAT is NP-complete. $\endgroup$ Oct 4 at 16:44
  • $\begingroup$ Can you re-phrase that? Are you saying the answer to my question is "no"? If so, I see no correlation between SAT's NP-completeness and there not being a more efficient format than CNF. That is, unless you are arguing that any other for could only be equally as efficient as CNF (but not more so). Even then, the support for such a position is tenuous at best as it rests on the assumption that P≠NP, which we do not know for certain. Even if P≠NP, it seems that a more efficient, yet still exponential time, algorithm (using a different form than CNF) could exist. Am I wrong in my reasoning? $\endgroup$ Oct 4 at 17:08
  • $\begingroup$ Perhaps you can formalize your question? It is too vague to answer at its present form. $\endgroup$ Oct 4 at 17:10
  • $\begingroup$ Ok, I will see if I can do that $\endgroup$ Oct 4 at 17:26
4
$\begingroup$

It's because this is close to how real-world problems tend to be expressed.

SAT has a lot of practical applications, from controlling power grids to integrated circuit layout. In pretty much every case, the problem is that you have a bunch of complex constraints that all need to be satisfied.

However you express each constraint, they ultimately get joined together with a logical "and". That's what "they all need to be satisfied" means.

For comparison, consider DNF. A sat problem expressed in DNF is, when you think about it, actually the answer to a SAT problem. Each conjunct is an assignment of variables joined together with logical "or", meaning that any one of those assignments solves the problem.

Many SAT solver front-ends will convert more complex constraints to CNF, but ultimately, all of the constraints have to be conjoined together.

$\endgroup$
10
  • $\begingroup$ Thank you for this. To re-state one of my questions: is is possible there is a better form that has not been found (i.e. a form that may not exactly model the real world but is easier for an algorithm to deal with)? $\endgroup$ Oct 4 at 14:35
  • $\begingroup$ Can you re-phrase that? Are you saying the answer to my question is "no"? If so, I see no correlation between SAT's NP-completeness and there not being a more efficient format than CNF. That is, unless you are arguing that any other for could only be equally as efficient as CNF (but not more so). Even then, the support for such a position is tenuous at best as it rests on the assumption that P≠NP, which we do not know for certain. Even if P≠NP, it seems that a more efficient, yet still exponential time, algorithm (using a different form than CNF) could exist. Am I wrong in my reasoning? $\endgroup$ Oct 4 at 17:07
  • $\begingroup$ @user3670473 Let me put it this way: DNF is a much more efficient representation for SAT problems, because you can literally just read off the answers. Unfortunately, converting CNF to DNF is NP-hard. $\endgroup$
    – Pseudonym
    Oct 4 at 22:57
  • $\begingroup$ @Pseudonym Conversion is not a decision problem. We can show that converting a CNF to DNF could require exponential blow-up. $\endgroup$ Oct 4 at 23:07
  • $\begingroup$ @Pseudonym I'm well aware DNF is much more efficient than CNF, and I am aware of the limits caused by the exponential time of conversion to DNF. I'm really just posing the question: is there another from, besides DNF or CNF, that may be more efficient than CNF and also easily convertible to? Or has the possibility of such a form been disproved? $\endgroup$ Oct 4 at 23:43

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.