Conjunction outside, disjunction inside
A variable p or its negation ¬p is a literal; p∨¬q is a clause, and (p∨¬q)∧(q∨r) is CNF. Every clause needs a true literal under the same assignment. Clause width counts literals within a clause, not the number of variables or clauses in the entire formula.
Different restrictions on this shape lead to different problems. 2-CNF bounds each clause at two literals, Horn CNF permits at most one positive literal per clause, and 3-CNF permits up to three literals. These are distinct structural restrictions.
Distribution and auxiliary variables
Distribution converts a∨(b∧c) into (a∨b)∧(a∨c), preserving equivalence over the original variables. Repeated distribution can duplicate subformulas, so it does not guarantee linear-size output. Practical encodings often name subformulas or circuit gates with fresh variables instead.
To represent z=a∧b, use (¬z∨a)∧(¬z∨b)∧(z∨¬a∨¬b), and add z when that subformula must hold. A satisfying original assignment extends to the auxiliary variables, and any satisfying encoded assignment restricts to a satisfying original assignment.
Equisatisfiability is a different guarantee
After fresh variables are introduced, the old and new formulas are not simply equivalent formulas over an unchanged vocabulary. The required guarantee is usually two-way preservation of satisfiability with recovery of original-variable values. Interpretation of models and proofs must account for that correspondence.
CNF alone does not ensure efficient solving. General CNF satisfiability is NP-complete, even at width three. Propagation simplifies forced choices but general inputs may still require branching. A uniform representation facilitates algorithms without eliminating the search problem.