Boolean logic
Conjunctive normal form
Abbreviated CNF
A Boolean formula written as an and of clauses.
Definition
Conjunctive normal form
Conjunctive normal form (CNF) is a conjunction of clauses, where each clause is a disjunction of literals.
Most CDCL solvers operate on CNF. A lowering procedure can introduce fresh variables while preserving whether the original formula is satisfiable.
01
Example
(a or b) and (not a or c) is a CNF formula with two clauses.
02
Important distinction
Equivalent-looking rewrites must preserve satisfiability; a malformed conversion can change the answer before the solver begins.
After reading this article, you should be able to
- Define CNF in the sense used on this site.
- Recognize CNF and evaluate all of its clauses under an assignment.