Resolution

Resolution is a rule of inference on clauses: from two clauses that contain some variable with opposite signs, it derives the clause made of all their other literals^[1]. From $a\vee b$ and $\neg b\vee c$, for example, it derives $a\vee c$. Resolution is the proof system of clausal logic: a refutation of a set of clauses is a derivation of the empty clause, which is false, and a set of clauses has a refutation exactly when it is unsatisfiable. SAT solvers are resolution engines. A DPLL search that ends in unsatisfiability is a resolution refutation in disguise, and every clause a CDCL solver learns is derived by resolution^[4]. In first-order logic, combined with unification, resolution became the basis of automated theorem proving and of Prolog^[1][13].

The clause below the line is the resolvent of the two premises on the pivot $x$. If both premises contain further complementary pairs, the resolvent is a tautology and is useless; if $C$ and $D$ are both empty, the resolvent is the empty clause $\square$.

The rule is sound: an assignment that satisfies both premises makes $x$ true or false; if true, $D\vee \neg x$ is satisfied by $D$, and if false, $C\vee x$ by $C$. So everything derived is a consequence, and deriving $\square$ shows unsatisfiability.

It is refutation complete: every unsatisfiable set of clauses has a refutation. One proof is the Davis–Putnam procedure^[2]. Eliminate a variable $x$ by replacing all clauses containing $x$ or $\neg x$ with all their resolvents on $x$. The new set is satisfiable if and only if the old one is, since any model of the resolvents can be extended by a value for $x$. Eliminating every variable leaves either no clauses, when the set was satisfiable, or the empty clause. Resolution is not complete in the stronger sense of deriving every consequence, since it cannot derive a tautology such as $x\vee \neg x$ from nothing, but refutation completeness suffices: to prove $F\models G$, refute $F\wedge \neg G$.

A refutation is a directed acyclic graph: its sources are input clauses, each other node is the resolvent of its two parents, and its sink is $\square$. Its size is the number of clauses. In a tree-like refutation each derived clause is used only once, so a lemma needed twice must be derived twice; in a general one, clauses can be reused. A DPLL search yields a tree-like refutation directly: each branch ends at an input clause falsified by the branch, and at each split the refutations of the two branches are resolved on the split variable.

(* Resolution proofs. A clause is a sorted list of literals. *)
type clause = int list
type proof = { clause : clause; step : step }
and step = Input of int | Resolve of int * proof * proof     (* pivot variable *)
 
let norm c = List.sort_uniq (fun a b -> compare (abs a, a) (abs b, b)) c
 
(* The resolvent of c1 (containing p) and c2 (containing -p). *)
let resolve p c1 c2 = norm (List.filter (fun l -> l <> p) c1 @ List.filter (fun l -> l <> -p) c2)
 
let falsified assignment c = List.for_all (fun l -> List.mem (-l) assignment) c
 
(* A tree-like refutation read off a DPLL search that splits on
   variables in order: each branch ends at an input clause falsified by
   the branch, and each split resolves the two subproofs on the split
   variable when both use it. *)
let refute (clauses : clause list) =
  let inputs = List.mapi (fun i c -> { clause = norm c; step = Input i }) clauses in
  let vars = List.sort_uniq compare (List.map abs (List.concat clauses)) in
  let rec go assignment = function
    | _ when List.exists (fun p -> falsified assignment p.clause) inputs ->
      Some (List.find (fun p -> falsified assignment p.clause) inputs)
    | [] -> None                                          (* a model: not refutable *)
    | v :: rest ->
      match go (v :: assignment) rest with
      | None -> None
      | Some p1 when not (List.mem (-v) p1.clause) -> Some p1   (* v was not needed *)
      | Some p1 ->
        match go (-v :: assignment) rest with
        | None -> None
        | Some p2 when not (List.mem v p2.clause) -> Some p2
        | Some p2 -> Some { clause = resolve v p2.clause p1.clause; step = Resolve (v, p2, p1) }
  in
  go [] vars
 
(* Pad to a width in characters, not bytes. *)
let pad n s =
  let chars = ref 0 in
  String.iter (fun ch -> if Char.code ch land 0xC0 <> 0x80 then incr chars) s;
  s ^ String.make (max 0 (n - !chars)) ' '
 
let rec size p = match p.step with Input _ -> 1 | Resolve (_, a, b) -> 1 + size a + size b
 
let show c = if c = [] then "□" else String.concat " ∨ " (List.map (fun l ->
    (if l < 0 then "¬" else "") ^ String.make 1 (Char.chr (Char.code 'a' + abs l - 1))) c)

open Resproof
 
(* Print a proof as numbered lines, premises first. *)
let print_proof p =
  let n = ref 0 in
  let rec go p =
    match p.step with
    | Input i -> incr n; Printf.printf "%2d  %s input clause %d\n" !n (pad 12 (show p.clause)) (i + 1); !n
    | Resolve (v, a, b) ->
      let i = go a in let j = go b in
      incr n; Printf.printf "%2d  %s resolve %d and %d on %s\n" !n (pad 12 (show p.clause)) i j (show [ v ]); !n
  in
  ignore (go p)

 1  a ∨ b        input clause 1
 2  a ∨ ¬b       input clause 2
 3  a            resolve 1 and 2 on b
 4  ¬a ∨ b       input clause 3
 5  ¬a ∨ ¬b      input clause 4
 6  ¬a           resolve 4 and 5 on b
 7  □            resolve 3 and 6 on a
--
 1  a            input clause 3
 2  ¬a ∨ b       input clause 1
 3  ¬b ∨ c       input clause 2
 4  ¬c           input clause 4
 5  ¬b           resolve 3 and 4 on c
 6  ¬a           resolve 2 and 5 on b
 7  □            resolve 1 and 6 on a
--
satisfiable: no refutation

Eliminating variables by resolution is complete but can multiply the number of clauses. A variable with $p$ positive and $n$ negative occurrences is replaced by up to $p\cdot n$ resolvents.

open Resproof
 
(* Davis–Putnam elimination: replace every clause containing v or -v by
   all non-tautological resolvents on v. *)
let tautology c = List.exists (fun l -> List.mem (-l) c) c
let eliminate v cs =
  let pos = List.filter (List.mem v) cs and neg = List.filter (List.mem (-v)) cs in
  let rest = List.filter (fun c -> not (List.mem v c || List.mem (-v) c)) cs in
  let resolvents = List.concat_map (fun p -> List.map (fun n -> resolve v p n) neg) pos in
  List.sort_uniq compare (rest @ List.filter (fun c -> not (tautology c)) resolvents)

pigeonhole, 4 in 3:
  clauses: 22 21 24 39 33 47 59 34 19 8 4 2 1
  empty clause derived after eliminating 12 variables
pigeonhole, 5 in 4:
  clauses: 45 44 52 96 284 246 606 2151 3280 1772 1013 629 249 136 73 42 16 8 4 2 1
  empty clause derived after eliminating 20 variables
chain a1 → a2 → ... → a12 with a1 and ¬a12:
  clauses: 13 12 11 10 9 8 7 6 5 4 3 2 1
  empty clause derived after eliminating 12 variables

On a chain of implications each elimination removes one clause, but on the pigeonhole formulas the intermediate sets grow to more than 3,000 clauses for five pigeons. This is why Logemann and Loveland replaced elimination with splitting in 1962. Modern solvers use elimination only as a preprocessing step, and only for variables whose elimination does not increase the number of clauses.

Every clause a CDCL solver learns is derived from the formula and earlier learned clauses by a chain of resolutions, so the sequence of learned clauses, ending with the empty clause, is a resolution proof in a compact form. Each clause in it can be checked by reverse unit propagation (RUP): assume all its literals are false and run unit propagation on the clauses known so far; if a conflict follows, the clause is implied^[10]. The DRAT format used in SAT competitions extends this with clause deletion and a stronger check for clauses that are not implied but preserve satisfiability^[11].

(* Checking a CDCL solver's learned clauses by reverse unit propagation:
   a clause C is implied if assuming every literal of C false and
   propagating the clauses known so far yields a conflict. *)
let rup (known : int list list) (c : int list) =
  let value = Hashtbl.create 64 in
  List.iter (fun l -> Hashtbl.replace value (abs l) (l < 0)) c;       (* make C false *)
  let lit_val l = match Hashtbl.find_opt value (abs l) with
    | None -> None | Some b -> Some (if l > 0 then b else not b) in
  let rec loop () =
    let changed = ref false and conflict = ref false in
    List.iter (fun cl ->
        if not !conflict && not (List.exists (fun l -> lit_val l = Some true) cl) then
          match List.filter (fun l -> lit_val l = None) cl with
          | [] -> conflict := true
          | [ l ] -> Hashtbl.replace value (abs l) (l > 0); changed := true
          | _ -> ()) known;
    !conflict || (!changed && loop ()) in
  loop ()

pigeonhole, 6 in 5       154 clauses in the proof,   154 verified,    1196 literals
pigeonhole, 7 in 6       758 clauses in the proof,   758 verified,    9981 literals
random 3-SAT, 60 vars     82 clauses in the proof,    82 verified,     386 literals

The relationship is exact in the other direction too. Pipatsrisawat and Darwiche showed that CDCL with restarts polynomially simulates general resolution^[14], while DPLL is limited to tree-like resolution^[4], which is exponentially weaker on some formulas^[5].

Proof complexity asks how long the shortest refutation of a formula must be. For resolution, several families require exponential size. Haken proved in 1985 that the pigeonhole formulas, stating that $n+1$ pigeons fit in $n$ holes, need refutations of size $2^{\Omega (n)}$^[3]. Urquhart proved the same in 1987 for Tseitin's parity formulas on expander graphs^[8], and Chvátal and Szemerédi showed in 1988 that random 3-CNF formulas with a linear number of clauses almost surely require exponential refutations^[6]. Ben-Sasson and Wigderson unified these results through width, the size of the largest clause in a refutation: a formula whose refutations all contain wide clauses has no short refutation^[7]. These bounds apply to every resolution-based solver. A further result limits what search can achieve even when short proofs exist: Atserias and Müller showed that finding a resolution refutation of size polynomial in the shortest one is NP-hard^[9].

Robinson's 1965 paper introduced resolution for first-order clauses, in which literals contain terms with variables. Two literals are resolved when they can be made complementary by a substitution, computed by his unification algorithm, and the resolvent carries the substitution^[1]. Combined with refinements such as ordered resolution and paramodulation for equality, this is the basis of saturation-based theorem provers. Kowalski observed that resolution restricted to Horn clauses, used in a goal-directed way, is a programming language; this is SLD resolution, the execution model of Prolog^[13].

Blake's thesis of 1937 contains the propositional rule in the form of the consensus of two terms, used to compute prime implicants^[12]. Davis and Putnam used resolution to eliminate variables in their satisfiability procedure of 1960^[2]. Robinson named the rule and gave its first-order form with unification in 1965^[1], which made it the dominant method of automated theorem proving for decades. Tseitin began the study of the lengths of resolution proofs in 1966, and Haken's pigeonhole lower bound of 1985 was the first exponential bound for unrestricted resolution^[3]. The connection between SAT solvers and resolution was made precise between 2004 and 2011^[4][14], and resolution-based proof checking became part of SAT competitions in the 2010s^[11].

• CDCLConflict-driven clause learning (CDCL) is the algorithm of modern SAT solvers. It extends DPLL backtracking search with three ideas: when propagation falsifies a clause, conflict analysis derives a new clause that explains the conflict and adds it to the formula; the solver then backjumps non-chronologically to the decision level at which the new clause forces a literal; and branching follows the variables involved in recent conflicts. With watched literals, restarts and clause deletion, CDCL solvers decide industrial formulas with millions of variables, and with restarts they are as strong as general resolution, exponentially stronger than DPLL.
• DPLLDPLL, the Davis–Putnam–Logemann–Loveland procedure, is the backtracking search algorithm for Boolean satisfiability on which all complete SAT solvers are built. It repeatedly simplifies a CNF formula by unit propagation and pure literal elimination, then chooses an unassigned variable and tries both of its values in turn, backtracking to the most recent choice when a clause becomes false. It is sound and complete, uses memory linear in the formula, and its runs on unsatisfiable formulas correspond to tree-like resolution proofs, which gives exponential lower bounds such as the n! − 1 decisions it needs for the pigeonhole formulas. Clause learning turned it into CDCL.
• First-UIP conflict analysisConflict analysis is the step of a CDCL SAT solver that explains a conflict by a new clause. Starting from the clause that became false, the solver repeatedly resolves it with the reason clauses of literals assigned at the current decision level, in reverse order of assignment, until only one literal of that level remains. That literal is the first unique implication point (UIP), a node through which every path from the decision to the conflict passes in the implication graph. The resulting clause is learned; it is implied by the formula, it forbids the combination of assignments that caused the conflict, and after backjumping to the second-highest level in it, it immediately propagates the negation of the UIP.
• Pigeonhole formulaThe pigeonhole formulas PHPⁿ⁺¹ₙ are CNF formulas stating that n + 1 pigeons can be placed in n holes with no two in the same hole. They are unsatisfiable, as the pigeonhole principle says, but Haken proved in 1985 that every resolution refutation of them has exponential size. Since SAT solvers based on DPLL and CDCL produce resolution proofs, they need exponential time on these small formulas, which makes the family the standard example of what resolution cannot do. Proof systems that can count, such as cutting planes and extended resolution, refute them in polynomial size.
• CNFA propositional formula is in conjunctive normal form (CNF) when it is a conjunction of clauses, each clause a disjunction of literals, and each literal a variable or its negation. Every formula is equivalent to one in CNF, but the equivalent CNF can be exponentially larger; the Tseitin transformation instead produces an equisatisfiable CNF of linear size by adding variables. CNF is the input format of SAT solvers and resolution provers, and restricted forms such as Horn clauses and 2-CNF can be solved in linear time.
• Craig interpolationCraig's interpolation theorem states that if a formula A implies a formula B, there is a formula I, the interpolant, built only from the symbols A and B have in common, such that A implies I and I implies B. In verification it is used in the equivalent refutation form: when A ∧ B is unsatisfiable, an interpolant is implied by A, inconsistent with B, and mentions only shared variables. For propositional logic, an interpolant can be computed from a resolution refutation of A ∧ B in linear time, which McMillan used in 2003 to build an unbounded model checker from a SAT solver.
• Tseitin transformationThe Tseitin transformation converts an arbitrary propositional formula or Boolean circuit into conjunctive normal form in linear time by introducing a new variable for each subformula and adding a few clauses that define it as the result of its operator: g ↔ a ∧ b becomes (¬g ∨ a), (¬g ∨ b) and (g ∨ ¬a ∨ ¬b). The result is not equivalent to the original formula but equisatisfiable, and every model of one extends or restricts to a model of the other. It is how SAT solvers receive circuits and structured formulas; the Plaisted–Greenbaum variant emits only the implications required by each subformula's polarity, roughly halving the clauses.
• 2-SAT2-SAT is Boolean satisfiability restricted to formulas in conjunctive normal form whose clauses have at most two literals. Unlike 3-SAT it is solvable in linear time: each clause (a or b) is a pair of implications, not a implies b and not b implies a, and the formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component of the resulting implication graph. A satisfying assignment can be read off a topological order of the components. Random 2-SAT has a sharp satisfiability threshold at one clause per variable.
• Pure literal eliminationPure literal elimination is a simplification rule for formulas in conjunctive normal form: if a variable occurs in the formula only positively, or only negatively, it can be set so that all its occurrences are true, and every clause containing it can be deleted, without changing whether the formula is satisfiable. It is one of the rules of the DPLL procedure. Modern CDCL solvers do not apply it during search, because detecting pure literals is expensive, but it survives in preprocessing, generalized by autarkies and blocked clause elimination.

1. [1]J. A. Robinson, “A machine-oriented logic based on the resolution principle”, Journal of the ACM 12 (1965).
2. [2]M. Davis, H. Putnam, “A computing procedure for quantification theory”, Journal of the ACM 7 (1960).
3. [3]A. Haken, “The intractability of resolution”, Theoretical Computer Science 39 (1985).
4. [4]P. Beame, H. Kautz, A. Sabharwal, “Towards understanding and harnessing the potential of clause learning”, Journal of Artificial Intelligence Research 22 (2004).
5. [5]E. Ben-Sasson, R. Impagliazzo, A. Wigderson, “Near optimal separation of tree-like and general resolution”, Combinatorica 24 (2004).
6. [6]V. Chvátal, E. Szemerédi, “Many hard examples for resolution”, Journal of the ACM 35 (1988).
7. [7]E. Ben-Sasson, A. Wigderson, “Short proofs are narrow — resolution made simple”, Journal of the ACM 48 (2001).
8. [8]A. Urquhart, “Hard examples for resolution”, Journal of the ACM 34 (1987).
9. [9]A. Atserias, M. Müller, “Automating resolution is NP-hard”, Journal of the ACM 67 (2020).
10. [10]E. Goldberg, Y. Novikov, “Verification of proofs of unsatisfiability for CNF formulas”, DATE (2003).
11. [11]N. Wetzler, M. J. H. Heule, W. A. Hunt, “DRAT-trim: efficient checking and trimming using expressive clausal proofs”, SAT (2014).
12. [12]A. Blake, Canonical Expressions in Boolean Algebra, PhD thesis, University of Chicago (1937).
13. [13]R. Kowalski, “Predicate logic as programming language”, IFIP Congress (1974).
14. [14]K. Pipatsrisawat, A. Darwiche, “On the power of clause-learning SAT solvers as resolution engines”, Artificial Intelligence 175 (2011).

last updated 28 September 2026