CNF

Conjunctive normal form (CNF) is a standard shape for propositional formulas: an AND of ORs. A literal is a variable $x$ or its negation $\neg x$; a clause is a disjunction of literals, such as $x_1\vee \neg x_2\vee x_3$; and a formula in CNF is a conjunction of clauses. A CNF formula is satisfied when every clause contains at least one true literal. Every propositional formula can be rewritten into an equivalent CNF formula, although sometimes only at exponential cost. For satisfiability, the Tseitin transformation produces a CNF formula of linear size that is satisfiable exactly when the original is. CNF is the input language of SAT solvers, written in the DIMACS format, and of resolution theorem provers, whose single inference rule works on clauses^[9].

A CNF formula is often treated as a set of clauses, and a clause as a set of literals. The empty clause is false, since none of its literals can be true, and the empty set of clauses is true. A clause containing both $x$ and $\neg x$ is a tautology and can be dropped. A unit clause has a single literal, which must be true in every model; this is the basis of unit propagation. The dual form, disjunctive normal form (DNF), is an OR of ANDs; the negation of a CNF formula is, by De Morgan's laws, a DNF formula, and vice versa. Satisfiability of a DNF formula is trivial, since it suffices to find one consistent conjunction, while satisfiability of CNF is NP-complete^[1].

A formula in which negation is applied only to variables is in negation normal form (NNF); De Morgan's laws and double-negation elimination convert any formula to NNF without growth. From NNF, a CNF follows by distributing disjunction over conjunction,

which is equivalence-preserving but can multiply the size: the clauses of $A\vee B$ are all pairwise unions of a clause of $A$ with a clause of $B$.

open Prop
 
(* Negation normal form: push negations down to the variables. *)
let rec nnf = function
  | Not (Not a) -> nnf a
  | Not (And (a, b)) -> Or (nnf (Not a), nnf (Not b))
  | Not (Or (a, b)) -> And (nnf (Not a), nnf (Not b))
  | And (a, b) -> And (nnf a, nnf b)
  | Or (a, b) -> Or (nnf a, nnf b)
  | f -> f
 
(* CNF by distributing ∨ over ∧: the clauses of a ∨ b are all unions of
   a clause of a with a clause of b. *)
let rec cnf = function
  | Var v -> [ [ v ] ]
  | Not (Var v) -> [ [ -v ] ]
  | And (a, b) -> cnf a @ cnf b
  | Or (a, b) -> List.concat_map (fun ca -> List.map (fun cb -> ca @ cb) (cnf b)) (cnf a)
  | Not _ -> invalid_arg "not in NNF"
 
(* (x1 ∧ x2) ∨ (x3 ∧ x4) ∨ ... ∨ (x(2n-1) ∧ x(2n)) *)
let pairs n =
  List.init n (fun i -> And (Var (2 * i + 1), Var (2 * i + 2)))
  |> List.fold_left (fun acc t -> match acc with None -> Some t | Some a -> Some (Or (a, t))) None
  |> Option.get

((x1 ∧ x2) ∨ (x3 ∧ x4))
= (x1 ∨ x3) ∧ (x1 ∨ x4) ∧ (x2 ∨ x3) ∧ (x2 ∨ x4)
n =  1:      2 clauses,       2 literals
n =  2:      4 clauses,       8 literals
n =  4:     16 clauses,      64 literals
n =  8:    256 clauses,    2048 literals
n = 12:   4096 clauses,   49152 literals
n = 16:  65536 clauses, 1048576 literals

The blow-up is unavoidable for some functions when equivalence is required. Any CNF for $(x_1\wedge x_2)\vee \cdots \vee (x_{2n-1}\wedge x_{2n})$ needs $2^n$ clauses, since each clause must contain a variable from every pair. The parity function $x_1\oplus \cdots \oplus x_n$ is worse: each clause of a CNF for it must mention every variable, since otherwise flipping an unmentioned variable would change the parity without changing the clause, so it needs $2^{n-1}$ clauses^[8]. Allowing new variables removes the problem. The Tseitin transformation names each subformula with a variable and needs a constant number of clauses per connective^[5]; the result is equisatisfiable rather than equivalent.

Some syntactic restrictions of CNF make satisfiability easy.

2-CNF

If every clause has at most two literals, each clause $a\vee b$ is a pair of implications $\neg a\to b$ and $\neg b\to a$, and the formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component of the implication graph, which can be checked in linear time^[2]. See 2-SAT.

Horn clauses

A Horn clause has at most one positive literal^[4]. A clause $\neg a\vee \neg b\vee c$ is the rule $a\wedge b\to c$, a unit $c$ is a fact, and a clause with no positive literal is a goal to be refuted. Satisfiability is decided by forward chaining: start with every variable false and set a variable true only when a rule whose premises are all true requires it. This produces the least model if there is one, and Dowling and Gallier showed that it can be done in linear time^[3]. Horn clauses are the logical basis of Prolog and Datalog.

(* Horn clauses have at most one positive literal. Start with every
   variable false and make a variable true only when a clause forces it;
   the result is the least model, or a clause with no positive literal
   is violated and the formula is unsatisfiable. *)
let horn_sat nvars (clauses : int list list) =
  let value = Array.make (nvars + 1) false in
  let violated c = List.for_all (fun l -> if l > 0 then not value.(l) else value.(-l)) c in
  let rec loop () =
    match List.find_opt violated clauses with
    | None -> Some value
    | Some c ->
      (match List.find_opt (fun l -> l > 0) c with
       | Some v -> value.(v) <- true; loop ()          (* forced: make the head true *)
       | None -> None)                                (* a goal clause fails *)
  in
  loop ()

least model: rain wet cold ice
unsatisfiable

k-CNF

For $k\ge 3$, $k$-CNF satisfiability is NP-complete; every CNF formula can be converted into an equisatisfiable 3-CNF by splitting long clauses with new variables, $(a\vee b\vee c\vee d)$ becoming $(a\vee b\vee y)\wedge (\neg y\vee c\vee d)$^[6].

CNF makes the facts that drive search local. A clause whose literals are all false is a conflict; a clause with one unassigned literal and the rest false forces that literal; a clause learned from a conflict is again a clause, so the solver's knowledge stays in one uniform representation. Resolution, the proof system implicit in DPLL and CDCL solvers, combines two clauses into a third^[9]. Encodings of problems into CNF are therefore an important craft of their own, and the choice of encoding for cardinality constraints, arithmetic or finite domains can change solving time by orders of magnitude^[7].

Normal forms for propositional formulas were standard in logic by the early twentieth century, as the conjunctive and disjunctive forms read off a truth table, with one clause or term per falsifying or satisfying row. Quine's work of 1952 on simplifying truth functions studied minimal normal forms^[10], and Horn identified the clauses that bear his name in 1951^[4]. Robinson's resolution principle of 1965 made clausal form the input of automated theorem provers^[9]. Cook stated his NP-completeness theorem for formulas in CNF in 1971^[1], and Karp's reduction to 3-CNF followed in 1972^[6]. The linear-time algorithms for 2-CNF and Horn formulas date from 1979 and 1984^[2][3].

• Tseitin transformationThe Tseitin transformation converts an arbitrary propositional formula or Boolean circuit into conjunctive normal form in linear time by introducing a new variable for each subformula and adding a few clauses that define it as the result of its operator: g ↔ a ∧ b becomes (¬g ∨ a), (¬g ∨ b) and (g ∨ ¬a ∨ ¬b). The result is not equivalent to the original formula but equisatisfiable, and every model of one extends or restricts to a model of the other. It is how SAT solvers receive circuits and structured formulas; the Plaisted–Greenbaum variant emits only the implications required by each subformula's polarity, roughly halving the clauses.
• SATThe Boolean satisfiability problem, SAT, asks whether some assignment of true and false to the variables of a propositional formula makes the formula true. It was the first problem shown to be NP-complete, so every problem in NP reduces to it, and no polynomial-time algorithm is known. In practice SAT solvers based on conflict-driven clause learning decide industrial instances with millions of variables, which has made SAT a general-purpose engine for hardware and software verification, planning, scheduling and combinatorics.
• DIMACS CNFDIMACS CNF is the standard plain-text format for Boolean formulas in conjunctive normal form, read by essentially every SAT solver. After optional comment lines beginning with c, a header p cnf V C gives the number of variables and clauses; each clause is then a list of non-zero integers, v for a variable and −v for its negation, terminated by 0. It was defined for the Second DIMACS Implementation Challenge in 1993 and has variants for quantified formulas (QDIMACS), weighted MaxSAT (WCNF) and unsatisfiability proofs (DRAT).
• Unit propagationUnit propagation is the inference rule at the core of SAT solvers: when every literal of a clause is false under the current partial assignment except one unassigned literal, that literal must be true. Applying the rule until nothing changes either extends the assignment or finds a clause with every literal false, a conflict. It decides satisfiability of Horn formulas on its own, it takes most of the running time of a modern CDCL solver, and it is implemented with two watched literals per clause so that only clauses that may have become unit are ever inspected.
• 2-SAT2-SAT is Boolean satisfiability restricted to formulas in conjunctive normal form whose clauses have at most two literals. Unlike 3-SAT it is solvable in linear time: each clause (a or b) is a pair of implications, not a implies b and not b implies a, and the formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component of the resulting implication graph. A satisfying assignment can be read off a topological order of the components. Random 2-SAT has a sharp satisfiability threshold at one clause per variable.
• ResolutionResolution is the inference rule that derives, from two clauses containing a variable with opposite signs, the clause of all their other literals: from C ∨ x and D ∨ ¬x, infer C ∨ D. It is sound and refutation complete for propositional logic, so a set of clauses is unsatisfiable exactly when the empty clause can be derived. Resolution is the proof system behind SAT solvers, whose runs on unsatisfiable formulas are resolution refutations, and behind first-order theorem provers and logic programming. Some formulas, such as the pigeonhole formulas, have only exponentially long resolution refutations.
• Bit-blastingBit-blasting decides formulas over fixed-width bit-vectors, the machine integers of programs and hardware, by translating every variable into one Boolean variable per bit and every operation into a Boolean circuit, then handing the resulting clauses to a SAT solver. Addition becomes a ripple-carry adder and multiplication a shift-and-add array of adders, encoded with the Tseitin transformation. It is complete and simple, and it is how SMT solvers handle bit-vectors after word-level simplification; its weak point is multiplication, whose circuits are large and hard for SAT solvers.
• Pure literal eliminationPure literal elimination is a simplification rule for formulas in conjunctive normal form: if a variable occurs in the formula only positively, or only negatively, it can be set so that all its occurrences are true, and every clause containing it can be deleted, without changing whether the formula is satisfiable. It is one of the rules of the DPLL procedure. Modern CDCL solvers do not apply it during search, because detecting pure literals is expensive, but it survives in preprocessing, generalized by autarkies and blocked clause elimination.

1. [1]S. A. Cook, “The complexity of theorem-proving procedures”, STOC (1971).
2. [2]B. Aspvall, M. F. Plass, R. E. Tarjan, “A linear-time algorithm for testing the truth of certain quantified Boolean formulas”, Information Processing Letters 8 (1979).
3. [3]W. F. Dowling, J. H. Gallier, “Linear-time algorithms for testing the satisfiability of propositional Horn formulae”, Journal of Logic Programming 1 (1984).
4. [4]A. Horn, “On sentences which are true of direct unions of algebras”, Journal of Symbolic Logic 16 (1951).
5. [5]G. S. Tseitin, “On the complexity of derivation in propositional calculus”, in Studies in Constructive Mathematics and Mathematical Logic, Part II (1968).
6. [6]R. M. Karp, “Reducibility among combinatorial problems”, in Complexity of Computer Computations, Plenum (1972).
7. [7]S. D. Prestwich, “CNF encodings”, in A. Biere et al. (eds.), Handbook of Satisfiability, IOS Press (2nd ed., 2021).
8. [8]I. Wegener, The Complexity of Boolean Functions, Wiley–Teubner (1987).
9. [9]J. A. Robinson, “A machine-oriented logic based on the resolution principle”, Journal of the ACM 12 (1965).
10. [10]W. V. O. Quine, “The problem of simplifying truth functions”, American Mathematical Monthly 59 (1952).

last updated 28 September 2026