CNF

Conjunctive normal form: a conjunction of clauses, each a disjunction of literals, where a literal is a variable or its negation, $F={\bigwedge }_{i=1}^m{\bigvee }_{j=1}^{k_i}{\ell }_{ij}$. It is the input format of SAT solvers. Every formula has an equivalent CNF, but it can be exponentially larger; the Tseitin transformation gives an equisatisfiable one of linear size instead.

A clause is satisfied when one of its literals is true, and the formula when every clause is. Solvers are built around that shape: a clause whose literals are all false but one forces the last one, which is unit propagation, and a clause whose literals are all false is a conflict.

An equivalent CNF comes from pushing negations down to the variables with De Morgan's laws and then distributing disjunction over conjunction:

Distribution is where the size goes. For ${\bigvee }_{i=1}^n(x_i\wedge y_i)$ each clause of the result picks one of $x_i,y_i$ from every term, which gives $2^n$ clauses, and no equivalent CNF has fewer.

type f = Var of int | Not of f | And of f * f | Or of f * f
 
let rec nnf = function
  | Var v -> Var v
  | Not (Var v) -> Not (Var v)
  | Not (Not a) -> nnf a
  | Not (And (a, b)) -> Or (nnf (Not a), nnf (Not b))
  | Not (Or (a, b)) -> And (nnf (Not a), nnf (Not b))
  | And (a, b) -> And (nnf a, nnf b)
  | Or (a, b) -> Or (nnf a, nnf b)
 
let rec distribute = function
  | Var v -> [ [ v ] ]
  | Not (Var v) -> [ [ -v ] ]
  | And (a, b) -> distribute a @ distribute b
  | Or (a, b) ->
      let ca = distribute a and cb = distribute b in
      List.concat_map (fun c -> List.map (fun d -> c @ d) cb) ca
  | Not _ -> assert false

 n   distributed   tseitin (clauses, variables)
 1             2         4, 3
 2             4        10, 7
 5            32        28, 19
10          1024        58, 39
15         32768        88, 59

Two restricted forms are decidable in polynomial time. In 2-CNF every clause has at most two literals; each clause $a\vee b$ gives the implications $\neg a\to b$ and $\neg b\to a$, and the formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component of the resulting graph, which is a linear-time check. In Horn CNF every clause has at most one positive literal, and unit propagation alone decides it. With three literals per clause the problem is already NP-complete.

• Tseitin transformationA translation of a propositional formula into CNF that introduces a fresh variable for each subformula and adds clauses saying the variable equals it. The result is equisatisfiable with the input rather than equivalent, and its size is linear in the input's.
• SATThe Boolean satisfiability problem: given a propositional formula, decide whether some assignment of true and false to its variables makes it true. It is the canonical NP-complete problem, and also one that modern solvers routinely settle for instances with millions of variables.
• DIMACS CNFThe plain-text interchange format for CNF instances: a header giving the variable and clause counts, then one clause per line as space-separated nonzero integers terminated by a zero, with a negative integer meaning a negated variable. Every SAT solver reads it, which is what makes solvers comparable at all.
• Unit propagationThe inference rule that does most of the work in a SAT solver: if every literal of a clause is false except one unassigned literal, that literal must be true. Applying it to fixpoint after each decision is where solvers spend the bulk of their time, which is why the data structure that finds unit clauses is the thing worth optimizing.
• ResolutionThe inference rule that combines two clauses containing a complementary pair of literals into one clause without them. It is refutation complete for propositional logic: a set of clauses is unsatisfiable exactly when the empty clause can be derived. DPLL runs correspond to tree-like resolution proofs, and CDCL runs to general ones.

1. [1]S. A. Cook, “The complexity of theorem-proving procedures”, STOC (1971).
2. [2]B. Aspvall, M. F. Plass, R. E. Tarjan, “A linear-time algorithm for testing the truth of certain quantified Boolean formulas”, Information Processing Letters 8 (1979).