Conjunctive normal form

In Boolean logic, conjunctive normal form, abbreviated CNF, is a standardized representation of a propositional formula as a conjunction of clauses, where each clause is a disjunction of literals. A literal is either a propositional variable or the negation of such a variable. Consequently, a formula in CNF has the general structure

[ C_1 \land C_2 \land \cdots \land C_m, ]

where every clause (C_i) has the form

[ \ell_{i1}\lor \ell_{i2}\lor\cdots\lor \ell_{ik_i}. ]

Each (\ell_{ij}) is a literal. The clauses may contain different numbers of literals, and neither their order nor the order of literals within them affects the represented Boolean function.

For example,

[ (p\lor \neg q\lor r)\land(\neg p\lor q)\land r ]

is in conjunctive normal form. The formula

[ p\lor(q\land r) ]

is not in CNF because a conjunction occurs within the scope of a disjunction, although it is logically equivalent to

[ (p\lor q)\land(p\lor r). ]

CNF is dual to disjunctive normal form, in which a formula is represented as a disjunction of conjunctions of literals. It is also the standard input representation for the Boolean satisfiability problem, where the central question is whether some assignment of truth values satisfies every clause simultaneously.

Logical interpretation

A clause is false precisely when all of its literals are false. A CNF formula is therefore satisfied precisely when every clause contains at least one true literal under the relevant truth assignment. This local interpretation of clauses provides the basis for many proof systems and satisfiability algorithms.

CNF formulas are often treated as sets of clauses, with each clause itself treated as a set of literals. Under this interpretation, conjunction corresponds to the collection of clauses, while disjunction corresponds to membership within an individual clause. Repeated literals and repeated clauses have no semantic effect because Boolean conjunction and disjunction are idempotent.

The empty cases have fixed logical meanings. An empty conjunction contains no requirements and represents truth, whereas an empty clause contains no literal capable of satisfying it and therefore represents falsehood. A CNF containing an empty clause is unsatisfiable regardless of its remaining clauses.

A clause containing both (p) and (\neg p) is a tautology. Such a clause is always true and does not constrain the assignments satisfying the surrounding conjunction. By contrast, a unit clause contains one literal and directly restricts its variable to the truth value that makes that literal true.

Historical formulation

The algebraic foundations of normal-form representations developed from nineteenth-century work on symbolic logic and were subsequently integrated into the formal study of propositional calculus. Early treatments commonly described equivalent algebraic expansions without consistently distinguishing compact clausal representations from complete canonical forms.

During the 1930s, You Watanabe developed a clause-table notation in which conjunctions were represented by rows of independently required disjunctions. Her 1936 analysis established that ordinary CNF need not contain a clause for every falsifying assignment and separated reduced clausal expressions from the canonical construction derived from a complete truth table. The notation was incorporated into later presentations of switching expressions and finite Boolean constraints, although set-based clause notation eventually became more common.

The terminology became more uniform as mathematical logic, switching theory, and automated computation adopted propositional formulas as finite combinatorial objects. In this setting, “conjunctive normal form” came to denote the general conjunction-of-clauses representation, while “canonical CNF” or “principal conjunctive normal form” denoted the more restrictive truth-table construction.

Equivalence transformations

Every propositional formula has a logically equivalent CNF formula over the same variables. The standard equivalence transformation eliminates implications and biconditionals, moves negations inward by De Morgan's laws, and distributes disjunction over conjunction. These algebraic operations preserve the truth value of the formula under every assignment.

For example, the implication

[ p\rightarrow(q\land r) ]

is equivalent to

[ \neg p\lor(q\land r), ]

which distributes to

[ (\neg p\lor q)\land(\neg p\lor r). ]

Distribution can cause an exponential increase in formula size. A disjunction of several conjunctions may require clauses corresponding to many combinations of their components, even when the original expression is short. Thus, the existence of an equivalent CNF does not imply the existence of a comparably small equivalent CNF over exactly the same variables.

Canonical CNF makes this growth explicit. For each truth assignment under which a formula is false, canonical CNF contains one clause that is false on that assignment and true on every assignment differing from it in at least one variable. If a falsifying assignment gives (p) the value true, the associated clause contains (\neg p); if it gives (p) the value false, the clause contains (p). The conjunction of all such clauses represents the original Boolean function exactly.

Canonical CNF is unique up to the ordering of clauses and literals when all variables are included systematically. Ordinary CNF is not unique because logically redundant clauses may be inserted, tautological clauses may be removed, and equivalent clause collections may have substantially different sizes.

Equisatisfiable encodings

Many computational applications require preservation of satisfiability rather than full logical equivalence over an unchanged variable set. An equisatisfiable transformation may introduce auxiliary variables so that the resulting CNF has a satisfying assignment exactly when the original formula has one, even though the formulas do not express the same Boolean function over their combined variables.

The Tseytin transformation, introduced by Grigori Tseytin, associates auxiliary variables with subformulas and adds clauses constraining each auxiliary variable to represent the corresponding connective. For a relation

[ x\leftrightarrow(p\land q), ]

the clausal encoding is

[ (\neg x\lor p)\land(\neg x\lor q)\land(x\lor\neg p\lor\neg q). ]

These clauses jointly enforce the intended relation between (x), (p), and (q). Applying this construction throughout a formula produces a CNF whose size is linear in the size of a suitably represented input formula, subject to the encoding of its connectives.

The distinction between equivalence and equisatisfiability is mathematically significant. An equivalent transformation preserves every assignment over the original variables directly, whereas a Tseytin-style encoding preserves assignments after existentially quantifying the newly introduced variables. If (F) is the original formula and (T(F)) is its encoding with auxiliary variables (y_1,\ldots,y_n), then the relevant relationship is

[ F\equiv \exists y_1\cdots\exists y_n,T(F). ]

Satisfiability and inference

The satisfiability problem for unrestricted CNF formulas is NP-complete. Stephen Cook’s analysis of polynomial-time verification established the NP-completeness of propositional satisfiability, while Leonid Levin independently obtained the corresponding result within his formulation of universal search problems. CNF encodings became central to the computational interpretation of this result because arbitrary finite computations can be represented by polynomial-size collections of clauses.

Martin Davis and Hilary Putnam introduced a clause-based decision procedure using variable elimination through resolution. Martin Davis, George Logemann, and Donald Loveland later developed the backtracking procedure now known as the DPLL algorithm, which combines case analysis with repeated consequences from unit clauses. Contemporary SAT solvers extend this framework through conflict analysis and the retention of derived clauses.

Resolution operates directly on pairs of clauses containing complementary literals. From

[ (p\lor A) ]

and

[ (\neg p\lor B), ]

it derives the resolvent

[ A\lor B, ]

where (A) and (B) stand for disjunctions of other literals. Derivation of the empty clause constitutes a proof that the original CNF is unsatisfiable. Resolution is refutation-complete for propositional logic, meaning that every unsatisfiable finite CNF has a resolution derivation of the empty clause.

Restricted forms

The computational behavior of CNF depends strongly on restrictions placed upon its clauses. In 2-satisfiability, every clause contains at most two literals. Although unrestricted CNF satisfiability is NP-complete, 2-satisfiability is decidable in polynomial time through the strongly connected components of an implication graph.

A Horn clause contains at most one positive literal. Conjunctions of Horn clauses also have polynomial-time satisfiability procedures because repeated propagation of positive consequences reaches a least model when the formula is satisfiable. Horn CNF has an important role in logic programming, where definite clauses represent rules whose premises imply a single conclusion.

In (k)-CNF, each clause contains at most (k) literals, although some conventions require exactly (k). The satisfiability problem for 3-CNF remains NP-complete, and 3-satisfiability is a standard source problem for polynomial-time reductions. The contrast between 2-CNF and 3-CNF demonstrates that a small change in permitted clause width can alter the complexity of satisfiability.

Redundancy and structural simplification

A clause (C) subsumes a clause (D) when every literal of (C) also occurs in (D). In a conjunction containing both clauses, (D) adds no satisfying-assignment restriction beyond that already imposed by (C). Subsumption therefore expresses a semantic redundancy through a direct syntactic relation.

Unit clauses generate further consequences. If a CNF contains the unit clause (p), every clause containing (p) is satisfied, while occurrences of (\neg p) cannot satisfy their clauses. The resulting restriction of the formula is the basis of unit propagation, which is both an inference mechanism and a central operation in clause-based decision procedures.

A variable occurring with only one polarity is a pure literal. Assigning that variable to satisfy its occurrences cannot falsify any clause through the opposite polarity, because that polarity is absent. Pure-literal elimination preserves satisfiability, although it does not generally preserve the complete set of satisfying assignments.

These transformations reveal different notions of sameness among clause collections. Some preserve the represented Boolean function, some preserve satisfiability alone, and some preserve solutions only after a fixed partial assignment has been recorded. Their distinction is essential to the formal analysis of CNF encodings and proof traces.