Unit propagation

Unit propagation is the inference rule at the core of every modern SAT solver. When all literals of a clause are false under the current partial assignment except one that is unassigned, the clause is unit, and that literal must be true in any satisfying extension of the assignment. Applying the rule repeatedly until nothing changes either extends the assignment with every forced literal or finds a clause whose literals are all false, a conflict. The rule goes back to the one-literal rule of Davis and Putnam^[1] and is also called Boolean constraint propagation (BCP). It decides the satisfiability of Horn formulas by itself^[3], it accounts for most of the running time of a CDCL solver^[5], and it is implemented with two watched literals per clause, so that the only clauses inspected are those that may just have become unit.

§ 01

The rule

A formula in conjunctive normal form is a set of clauses, each a disjunction of literals. Under a partial assignment, a clause is satisfied if one of its literals is true, conflicting if all are false, unit if all but one are false and that one is unassigned, and unresolved otherwise. The unit rule, written as an inference with $C$ the rest of the clause:

\frac{C \lor ℓ \neg C}{ℓ}

where $\neg C$ means every literal of $C$ is false. Equivalently it is resolution with a unit clause: from $ℓ$ and $\neg ℓ \lor D$ derive $D$ , which is why the rule is also called unit resolution. Propagation applies it until a fixed point, and the result does not depend on the order in which unit clauses are processed, except that when there is a conflict, which conflicting clause is found first may differ^[8].

Unit propagation on a list of clauses, printing each inference.

(* Unit propagation on a clause list, printing each inference. Literals
   are non-zero integers: v is the variable v, -v its negation. *)
let value a l = match List.assoc_opt (abs l) a with None -> None | Some b -> Some (if l > 0 then b else not b)
 
let rec propagate cs a =
  let rec scan = function
    | [] -> `Fixpoint
    | c :: rest ->
        if List.exists (fun l -> value a l = Some true) c then scan rest
        else match List.filter (fun l -> value a l = None) c with
          | [] -> `Conflict c
          | [ l ] -> `Unit (l, c)
          | _ -> scan rest
  in
  match scan cs with
  | `Fixpoint -> Some a
  | `Conflict c -> Printf.printf "  conflict: every literal of %s is false\n" (show c); None
  | `Unit (l, c) -> Printf.printf "  %s is unit, so %d\n" (show c) l; propagate cs ((abs l, l > 0) :: a)
 
and show c = "(" ^ String.concat " v " (List.map string_of_int c) ^ ")"

Running it.

decide 1:
  (-1 v 2) is unit, so 2
  (-2 v 3) is unit, so 3
  (-1 v -3 v 4) is unit, so 4
  (-4 v -5) is unit, so -5
  (-4 v 5 v 6) is unit, so 6
  (-2 v -6 v 7) is unit, so 7
  conflict: every literal of (-7 v -3 v -1) is false
decide -1, then 5:
  (-4 v -5) is unit, so -4
  no conflict

Deciding $x_{1}$ true forces six more literals in a chain and ends in a conflict, which proves that $x_{1}$ must be false. A solver that learns from the conflict records a clause that says so; see conflict analysis. Deciding $x_{1}$ false forces nothing, and a later decision on $x_{5}$ forces $\neg x_{4}$ .

§ 02

Power and limits

Unit propagation is sound but incomplete: a formula can be unsatisfiable without propagation finding a conflict, for example $(a \lor b) \land (a \lor \neg b) \land (\neg a \lor b) \land (\neg a \lor \neg b)$ , which has no unit clause at all. On Horn formulas, where each clause has at most one positive literal, it is complete: propagate from the unit clauses, and if no conflict arises, setting every remaining variable false satisfies the formula. With counters on the clauses this takes time linear in the size of the formula^[3]. Deciding whether propagation derives a literal is P-complete^[10], which suggests that it cannot be parallelized well, and in practice it is the part of a solver that is hardest to speed up by adding processors.

Propagation is used for more than search. Failed-literal probing tentatively assigns a literal, propagates, and if a conflict follows, fixes the literal's negation; lookahead solvers use the number of literals a decision would force to choose the decision^[11].

§ 03

In DPLL and CDCL

The Davis–Putnam–Logemann–Loveland procedure alternates propagation with decisions and backtracks on conflicts^[2]; see DPLL. CDCL solvers keep the same loop but record, for each propagated literal, the clause that forced it, its reason. The reasons form an implication graph, from which conflict analysis derives a learned clause, and non-chronological backjumping undoes several decisions at once^[7]. Because learned clauses accumulate, the clause database grows to many times the size of the input, and most of the solver's time goes into finding which of those clauses have become unit after each assignment. The Chaff authors reported that propagation took around 90 per cent of the running time of their solver^[5].

§ 04

Watched literals

Scanning every clause after every assignment costs time proportional to the size of the database, most of it spent on clauses that cannot be affected. A clause can only become unit or conflicting when the number of its non-false literals drops to one or zero, so it suffices to track two of its non-false literals, the watches. The clause needs attention only when one of its watches becomes false. The solver then looks for another non-false literal to watch; if there is none, the clause is unit, forcing the other watch, or conflicting^[5].

Scanning every clause, and two watched literals, as propagation engines of the same DPLL search.

(* Two propagation engines inside the same DPLL search, counting how many
   times a clause is inspected. Literals are non-zero integers. *)
type solver = {
  n : int;
  clauses : int array array;
  assign : int array;               (* by variable: 0 unassigned, 1 true, -1 false *)
  trail : int array;                (* assigned literals in order *)
  mutable len : int;
  mutable qhead : int;              (* trail entries not yet propagated *)
  watches : int list array;         (* clauses watching each literal *)
  mutable visits : int;
}
 
let idx l = if l > 0 then 2 * l else (2 * -l) + 1
let value s l = let v = s.assign.(abs l) in if l > 0 then v else -v
let set s l = s.assign.(abs l) <- (if l > 0 then 1 else -1); s.trail.(s.len) <- l; s.len <- s.len + 1
let undo_to s mark =
  for i = s.len - 1 downto mark do s.assign.(abs s.trail.(i)) <- 0 done;
  s.len <- mark; s.qhead <- mark
 
let create n clauses =
  let s = { n; clauses; assign = Array.make (n + 1) 0; trail = Array.make (n + 1) 0; len = 0; qhead = 0;
            watches = Array.make ((2 * n) + 2) []; visits = 0 } in
  Array.iteri (fun ci c -> List.iter (fun l -> s.watches.(idx l) <- ci :: s.watches.(idx l)) [ c.(0); c.(1) ]) clauses;
  s
 
(* Engine 1: inspect every clause, repeatedly, until nothing changes. *)
let propagate_scan s =
  let rec loop () =
    let changed = ref false and conflict = ref false in
    Array.iter (fun c ->
      if not !conflict then begin
        s.visits <- s.visits + 1;
        if not (Array.exists (fun l -> value s l = 1) c) then
          match List.filter (fun l -> value s l = 0) (Array.to_list c) with
          | [] -> conflict := true
          | [ l ] -> set s l; changed := true
          | _ -> ()
      end) s.clauses;
    if !conflict then false else if !changed then loop () else true
  in
  loop ()
 
(* Engine 2: two watched literals, c.(0) and c.(1) of each clause. When a
   literal becomes false, only the clauses watching it are inspected. *)
let propagate_watched s =
  let ok = ref true in
  while !ok && s.qhead < s.len do
    let falsified = - s.trail.(s.qhead) in
    s.qhead <- s.qhead + 1;
    let pending = ref s.watches.(idx falsified) in
    s.watches.(idx falsified) <- [];
    while !pending <> [] do
      let ci = List.hd !pending in
      pending := List.tl !pending;
      s.visits <- s.visits + 1;
      let c = s.clauses.(ci) in
      if c.(0) = falsified then (c.(0) <- c.(1); c.(1) <- falsified);
      let keep () = s.watches.(idx falsified) <- ci :: s.watches.(idx falsified) in
      if value s c.(0) = 1 then keep ()
      else begin
        let k = ref 2 in
        while !k < Array.length c && value s c.(!k) = -1 do incr k done;
        if !k < Array.length c then begin
          c.(1) <- c.(!k); c.(!k) <- falsified;
          s.watches.(idx c.(1)) <- ci :: s.watches.(idx c.(1))
        end
        else begin
          keep ();
          if value s c.(0) = -1 then begin
            ok := false;
            s.watches.(idx falsified) <- !pending @ s.watches.(idx falsified);
            pending := []
          end
          else set s c.(0)
        end
      end
    done
  done;
  !ok
 
(* Plain DPLL: propagate, then branch on the first unassigned variable. *)
let rec dpll s propagate decisions =
  if not (propagate s) then false
  else
    let rec first v = if v > s.n then None else if s.assign.(v) = 0 then Some v else first (v + 1) in
    match first 1 with
    | None -> true
    | Some v ->
        let mark = s.len in
        incr decisions;
        set s v;
        dpll s propagate decisions || (undo_to s mark; set s (-v); dpll s propagate decisions) || (undo_to s mark; false)

Random 3-SAT at the ratio 4.26 of clauses to variables, where instances are hardest. Both engines make the same decisions and reach the same result.

n    m     result  decisions    visits (scan) visits (watched)
40   170    UNSAT        101            67940             4618
60   255      SAT        478           460809            22673
80   340      SAT        688           927256            38746
100  426      SAT       5031          9599153           298492

The watched engine inspects between about 15 and 32 times fewer clauses on these small instances, and the gap grows with the size of the formula, since the scanning engine's cost per assignment is proportional to the number of clauses while the watched engine's is proportional to the number of clauses watching the literal that became false. A second advantage is that backtracking needs no work on the clauses: the watches remain valid when assignments are undone, because undoing only makes false literals unassigned. Counter-based schemes, in contrast, must restore every counter they changed^[9].

Refinements

Zhang's SATO used head and tail pointers into each clause, which moved in one direction and had to be reset on backtracking^[4]. Chaff's watches can move to any non-false literal and need no reset^[5]. Chu, Harwood and Stuckey proposed storing with each watch a blocker, another literal of the clause; if the blocker is true the clause is satisfied and need not be loaded from memory at all, which saves cache misses^[12]. MiniSat, whose compact design became the basis of many later solvers^[6], adopted them. Solvers also keep binary clauses in separate watch lists, since a binary clause that loses a watch is always unit or conflicting.

§ 05

In SMT solvers

In DPLL(T) the same propagation runs on the Boolean abstraction of the formula, and theory solvers add theory propagation: when the literals assigned so far imply another literal in the theory, for example $x \leq 3$ implying $x \leq 5$ , it is assigned with an explanation clause as its reason, so conflict analysis treats it like any unit-propagated literal^[8].

§ 06

History

Davis and Putnam's 1960 procedure included the one-literal rule^[1], and it was kept in the backtracking version of Davis, Logemann and Loveland in 1962^[2]. Dowling and Gallier gave the linear-time algorithm for Horn formulas in 1984^[3]. GRASP introduced conflict analysis on the implication graph built by propagation in 1996–1999^[7], Zhang's SATO used head and tail pointers in 1997^[4], and Chaff introduced two watched literals in 2001^[5]. MiniSat's compact implementation followed in 2003^[6], and blocking literals in 2008–2009^[12].