CNFs

CNF stands for conjunctive normal form, a standard way to represent logical formulas in propositional logic and, with additional steps, in first-order logic. A CNF formula is a conjunction (AND) of one or more clauses, where each clause is a disjunction (OR) of literals. A literal is a propositional variable or its negation.

In a CNF formula, the overall structure is a set of clauses joined by AND, and within each clause the literals are joined by OR. For example, (A ∨ ¬B) ∧ (B ∨ C ∨ ¬D) is in CNF. CNF is central to many topics in computer science because many decision procedures, such as SAT solvers, operate on CNF formulas.

SAT problems are often specified as CNF, and 3-CNF, where each clause has at most three literals, is a widely studied subclass (3-SAT is NP-complete). Converting an arbitrary propositional formula to CNF is possible, but naive conversions can cause a large increase in size. The Tseitin transformation is a common method that introduces new variables to produce an equisatisfiable CNF with only a linear increase in length relative to the original formula, making it more practical for SAT solving.

In first-order logic, CNF consists of universal clauses formed by disjunctions of literals (which may be atomic formulas or their negations). Achieving CNF typically involves skolemization, removing existentials, and moving quantifiers to a prenex form before distributing disjunctions over conjunctions.

CNF remains a foundational representation in automated reasoning, model checking, and software verification due to its amenability to algorithmic handling.