CNF formula

A CNF formula is a logical statement in a specific normal form — that is, in a prescribed, uniform structure. It consists of several groups of conditions that must all hold simultaneously. Within each group, at least one condition must be satisfied. Groups are thus connected with AND, and the contents of a group are connected with OR. A single condition is always a variable or its negation — for example, “it is raining” or “it is not raining”. The abbreviation CNF stands for the term “conjunctive normal form”.

CNF as the common language of logic software

Many problems in computer science and mathematics can be formulated as a question: Is there an assignment of variables that makes a particular statement true? Such questions are called satisfiability problems. CNF formulas are the standard for this because their structure is uniform and predictable. An algorithm that understands CNF can thereby serve as a single general-purpose tool for a hundred different problems.

There is also a theoretical reason: any arbitrary logical statement can be mechanically converted into an equivalent CNF formula. “Equivalent” here means: the new formula is satisfiable exactly if the original one was. This makes CNF a universal intermediate format — comparable to how music can be stored in various formats, but MP3 is the format that all players understand.

The structure of a CNF formula in detail

The basic building blocks are called literals. A literal is either a variable (e.g., A) or its negation (¬A, read as “not A”). Several literals connected with OR form a clause. For example, (A ∨ ¬B ∨ C) is a clause — it is already true as soon as at least one of the three literals is true. A CNF formula, finally, is a chain of such clauses connected with AND.

A concrete example: (A ∨ B) ∧ (¬A ∨ C) ∧ (¬B ∨ ¬C). This formula has three clauses. It is satisfiable if values for A, B, and C can be found such that each of the three clauses becomes true. With A = true, B = false, C = true, this works. A common misconception is equating CNF with a simple list of conditions — what matters is the nesting: OR within the clauses, AND between the clauses, never the other way around.

An important special form is 3-CNF: here, each clause may contain exactly three literals. This sounds like a restriction, but it is theoretically just as expressive as arbitrary CNF. The question of whether a 3-CNF formula is satisfiable is called 3-SAT and is one of the best-known problems in theoretical computer science.

CNF in practice: SAT solvers and AI planning

Programs that check whether a CNF formula is satisfiable are called SAT solvers. They are used in chip design to check circuits for errors, and in software analysis to verify safety-critical code. Modern SAT solvers can solve formulas with millions of clauses in seconds — even though the problem theoretically belongs to the hardest of all.

CNF also appears in AI. Planning algorithms — for example, for robots or automated logistics systems — translate goals and rules into CNF formulas and then ask a SAT solver whether a solution exists. Anyone reading news about chip design, formal verification, or automated reasoning will sooner or later come across this format. CNF itself is rarely the topic, but it is almost always the tool behind it.