Why is SAT based on the CNF?

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.