CNF — The Conjunctive Normal Form¶

Most modern SAT solvers expect that their input formula is in conjunctive normal form (CNF) because such formulas

can be represented with compact data structures that
allow efficient constraint propagation and conflict-driven learning (as explained later in the section Conflict-driven clause learning (CDCL) SAT solvers).

Definition: Literals, clauses, CNF

A literal is a variable or the negation of a variable.

A clause is a disjunction \( (l_1 \lor … \lor l_k) \) of literals \( l_i \).

A formula is in conjunctive normal form (CNF) if it is a conjunction \( C_1 \land … \land C_m \) of clauses \( C_i \).

Example

The formula \[(a \lor \neg b) \land (\neg a \lor b \lor \neg c) \land (\neg a)\] is in CNF while \( (a \lor (\neg b \land c)) \land (\neg a) \) is not in CNF.

Observe the special cases:

The empty clause \( () \) always evaluates to false.
The empty CNF formula with no clauses is satisfiable.

Using CNF formulas instead of generic formulas does not limit the expressive power of the logic. We will later, in the section CNF Translations, see that all formulas can be translated to CNF. Although expressing constraints in CNF directly can be more tedious than with unrestricted formulas, several important constraint types are easily expressible in CNF.

Example: At-least one in CNF

Expressing a constraint that at least one of the literals in a set \( L = \Set{l_1,…,l_k} \) should be true is easy in CNF: just add the clause \( (l_1 \lor … \lor l_k) \).

Example: At-most-one in CNF

Forcing that at most one of the literals in \( L = \Set{l_1,…,l_k} \) is true can be stated in formulas as follows: \( \bigwedge_{l,l’ \in L, l \neq l’}\neg(l \land l’) \). As \( \neg(l \land l’) \) is equivalent to \( (\neg l \lor \neg l’) \), the CNF version is \[\bigwedge_{l,l’ \in L, l \neq l’}(\neg l \lor \neg l’)\] Note that the formulas above have a quadratic amount of literals in the size of the set \( L \). More compact encodings exist when auxiliary variables are allowed.

Example: If-then in CNF

Constraints of the form \( (l_1 \land .. \land l_k) \Implies (l’_1 \land … \land l’_m) \) are also common. In CNF, we can express them with \( m \) clauses as follows: \[(\neg l_1 \lor … \lor \neg l_k \lor l’_1) \land … \land (\neg l_1 \lor … \lor \neg l_k \lor l’_m)\] Similarly, a constraint of the form \( (l_1 \land .. \land l_k) \Implies (l’_1 \lor … \lor l’_m) \) directly translates to one clause \[(\neg l_1 \lor … \lor \neg l_k \lor l’_1 \lor … \lor l’_m)\]