Pure literal elimination

Pure literal elimination is a rule for simplifying a formula in conjunctive normal form. A literal is pure if its negation does not occur in the formula. Making a pure literal true satisfies every clause in which it occurs and falsifies no clause, since its negation appears nowhere, so those clauses can be deleted and the rest of the formula is untouched^[1]. The simplified formula is satisfiable exactly when the original is. Deleting clauses can make further literals pure, so the rule is applied repeatedly. Davis and Putnam included it in their procedure of 1960 as the affirmative–negative rule^[2], and it is one of the three rules of DPLL, alongside unit propagation and splitting.

If $\ell$ occurs in $F$ and $\neg \ell$ does not, then

One direction is immediate, since $F{|}_{\ell }$ is a subset of $F$. For the other, take a model of $F{|}_{\ell }$ and change it to make $\ell$ true: the deleted clauses are now satisfied, and the remaining clauses do not contain $\neg \ell$, so none of them is falsified by the change. Unlike unit propagation, the rule does not preserve all models. It commits to one value even though the other value might also have led to a solution, which is harmless for deciding satisfiability but wrong for counting models or enumerating them.

(* Pure literal elimination as a preprocessing step: while some literal
   occurs only with one sign, make it true and drop its clauses. *)
let rec eliminate_pure cs removed =
  let lits = List.sort_uniq compare (List.concat cs) in
  match List.find_opt (fun l -> not (List.mem (-l) lits)) lits with
  | None -> (cs, removed)
  | Some l -> eliminate_pure (List.filter (fun c -> not (List.mem l c)) cs) (l :: removed)
 
(* Blocked clauses generalize this. A clause C is blocked on its literal
   l if every resolvent of C on l with a clause containing -l is a
   tautology. Removing a blocked clause preserves satisfiability. *)
let tautology c = List.exists (fun l -> List.mem (-l) c) c
let blocked cs c =
  List.exists (fun l ->
      List.for_all (fun d ->
          not (List.mem (-l) d)
          || tautology (List.filter (( <> ) l) c @ List.filter (( <> ) (-l)) d)) cs) c
 
let rec eliminate_blocked cs =
  match List.find_opt (blocked cs) cs with
  | None -> cs
  | Some c -> eliminate_blocked (List.filter (( != ) c) cs)

open Pure

pure literals set: 5 4 1 -2
clauses left: 0 of 4
g: pure literals 0, clauses left after blocked clause elimination: 0 of 4

In DPLL the rule is applied after unit propagation, before splitting^[1]. It never needs to be undone for its own sake, and it can shorten the search considerably: on the pigeonhole formulas it reduces the number of decisions by a factor that grows with the size, from 374 to 119 for six pigeons (see DPLL). Conflict-driven solvers omit it^[7]. With watched literals, a solver does not know how many clauses contain each literal or which clauses are satisfied, and maintaining occurrence counts would cost time on every assignment and every backtrack, which is exactly what watched literals were designed to avoid. The rule also combines awkwardly with clause learning, because learned clauses can reintroduce a literal's negation.

Before search, occurrence lists are available and the rule is cheap. On random formulas its effect depends on the density.

open Pure

clauses/var  removed by pure  removed by blocked  agree with solver
    1.00           99.2%             100.0%         true
    2.00           26.1%              35.6%         true
    3.00            4.0%               4.9%         true
    4.26            0.4%               0.5%         true

Sparse formulas collapse, because most variables occur few times and often with one sign; near the satisfiability threshold almost every variable occurs with both signs and the rule removes almost nothing. On structured formulas, such as those produced by the Plaisted–Greenbaum encoding, whose one-sided definitions create pure literals by design, it is more useful.

Autarkies

An autarky is a partial assignment that satisfies every clause it touches: each clause either contains a true literal under the assignment or mentions none of its variables. Applying an autarky and deleting the satisfied clauses preserves satisfiability, by the same argument as for pure literals, which are the one-variable autarkies. Monien and Speckenmeyer introduced autarkies in 1985 to obtain a satisfiability algorithm faster than $2^n$^[3], and Kullmann developed their theory^[8].

Blocked clauses

A clause $C$ is blocked on a literal $\ell \in C$ if every resolvent of $C$ on $\ell$ with a clause containing $\neg \ell$ is a tautology. A blocked clause can be deleted without affecting satisfiability^[4]. Every clause containing a pure literal is blocked on it, vacuously, since there are no clauses to resolve with, so blocked clause elimination subsumes pure literal elimination. Järvisalo, Biere and Heule showed that it also removes much of the redundancy that CNF encodings of circuits introduce, and it is implemented in modern preprocessors together with bounded variable elimination^[5][6].

The rule appeared as the “affirmative–negative rule” in Davis and Putnam's procedure of 1960^[2] and was kept in the Davis–Logemann–Loveland version of 1962^[1]. It was standard in DPLL-based solvers through the 1990s. The clause-learning solvers of the 2000s dropped it from the search loop^[7], while the theory of autarkies and Kullmann's blocked clauses^[8][4] generalized it, and blocked clause elimination entered SAT preprocessing in 2010^[5].

• 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.
• Unit propagationUnit propagation is the inference rule at the core of SAT solvers: when every literal of a clause is false under the current partial assignment except one unassigned literal, that literal must be true. Applying the rule until nothing changes either extends the assignment or finds a clause with every literal false, a conflict. It decides satisfiability of Horn formulas on its own, it takes most of the running time of a modern CDCL solver, and it is implemented with two watched literals per clause so that only clauses that may have become unit are ever inspected.
• ResolutionResolution is the inference rule that derives, from two clauses containing a variable with opposite signs, the clause of all their other literals: from C ∨ x and D ∨ ¬x, infer C ∨ D. It is sound and refutation complete for propositional logic, so a set of clauses is unsatisfiable exactly when the empty clause can be derived. Resolution is the proof system behind SAT solvers, whose runs on unsatisfiable formulas are resolution refutations, and behind first-order theorem provers and logic programming. Some formulas, such as the pigeonhole formulas, have only exponentially long resolution refutations.
• 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.

• Implementing SAT in OCaml Part 1CNF, unit propagation, a full recursive DPLL solver, pure literal elimination, a DIMACS parser, and a command-line driver.

1. [1]M. Davis, G. Logemann, D. Loveland, “A machine program for theorem-proving”, Communications of the ACM 5 (1962).
2. [2]M. Davis, H. Putnam, “A computing procedure for quantification theory”, Journal of the ACM 7 (1960).
3. [3]B. Monien, E. Speckenmeyer, “Solving satisfiability in less than 2ⁿ steps”, Discrete Applied Mathematics 10 (1985).
4. [4]O. Kullmann, “On a generalization of extended resolution”, Discrete Applied Mathematics 96–97 (1999).
5. [5]M. Järvisalo, A. Biere, M. J. H. Heule, “Blocked clause elimination”, TACAS (2010).
6. [6]N. Eén, A. Biere, “Effective preprocessing in SAT through variable and clause elimination”, SAT (2005).
7. [7]J. Marques-Silva, I. Lynce, S. Malik, “Conflict-driven clause learning SAT solvers”, in A. Biere et al. (eds.), Handbook of Satisfiability, IOS Press (2009).
8. [8]O. Kullmann, “Investigations on autark assignments”, Discrete Applied Mathematics 107 (2000).

last updated 28 September 2026