Watched literals

Watched literals are the scheme by which conflict-driven SAT solvers find the clauses that unit propagation must act on^[1]. A clause matters to propagation only when all but one of its literals are false, which makes it unit, or all are false, which is a conflict. As long as two of its literals are not false, neither can happen. So each clause keeps two watched literals, not false under the current assignment, and is listed in the watch list of each. When a literal becomes false, the solver visits only the clauses watching it; each looks for another non-false literal to watch instead, and only if there is none does the clause become unit on its other watch or, if that is false too, a conflict. The scheme was introduced by the Chaff solver in 2001^[1], refining the head and tail pointers of the SATO solver^[2], and is used by essentially every CDCL solver.

§ 01

The invariant

For a clause $C$ of at least two literals, with watches $w_{1}, w_{2} \in C$ , the scheme maintains, after propagation has finished,

if w_{1} or w_{2} is false, then the other is true, or every literal of C is false

A clause whose watches are both non-false can have no unit or conflict status, however many of its other literals are false. When $w_{1}$ becomes false, the clause is visited. If $w_{2}$ is true, the clause is satisfied and nothing needs to change. Otherwise the solver scans the other literals for one that is not false; if it finds one, it watches it instead of $w_{1}$ . If it finds none, all literals except $w_{2}$ are false: the clause is unit and $w_{2}$ is assigned, or $w_{2}$ is false as well and the clause is a conflict^[1].

A clause of five literals, with its watches marked above. When b becomes false, the clause is visited and the watch moves to d. Then c and e become false without any work, since they are not watched. When d becomes false no replacement exists, so the clause is unit and ¬a is forced.

§ 02

Why backtracking is free

Backtracking unassigns literals, which can only turn false literals into unassigned ones. A watched literal that was not false stays not false, so every clause still satisfies the invariant with the same watches, and nothing needs to be updated. A solver that keeps counters of true and false literals per clause, the scheme used before Chaff, must update every clause containing a variable both when the variable is assigned and when it is unassigned^[6]. Watching also reduces the work on assignment: making $x$ false visits only the clauses currently watching $x$ , not all clauses containing it, and making $x$ true visits nothing at all.

A counter-based engine and a watched-literal engine behind the same interface, each counting clause visits, with a DPLL search on top.

(* Two propagation engines behind one interface, counting how many
   clause visits each makes when literals are assigned and when they are
   unassigned on backtracking. Literals are non-zero integers. *)
type counts = { mutable on_assign : int; mutable on_backtrack : int }
 
module type ENGINE = sig
  type t
  val create : int -> int array array -> counts -> t
  val assign : t -> int -> bool          (* false on conflict *)
  val unassign_to : t -> int -> unit     (* backtrack to a trail length *)
  val trail_length : t -> int
  val value : t -> int -> int
end
 
let idx l = if l > 0 then 2 * l else (2 * -l) + 1
 
(* Counters: every clause knows how many of its literals are true and how
   many false, so every assignment updates every clause the variable
   occurs in, and backtracking must undo each update. *)
module Counters : ENGINE = struct
  type t = { cls : int array array; occ : int list array; tru : int array; fls : int array;
             value : int array; trail : int Stack.t; c : counts }
  let create n cls c =
    let occ = Array.make ((2 * n) + 2) [] in
    Array.iteri (fun i cl -> Array.iter (fun l -> occ.(idx l) <- i :: occ.(idx l)) cl) cls;
    { cls; occ; tru = Array.make (Array.length cls) 0; fls = Array.make (Array.length cls) 0;
      value = Array.make (n + 1) 0; trail = Stack.create (); c }
  let value s l = let v = s.value.(abs l) in if l > 0 then v else -v
  let trail_length s = Stack.length s.trail
  let rec assign s l =
    if value s l = 1 then true else if value s l = -1 then false else begin
      s.value.(abs l) <- (if l > 0 then 1 else -1); Stack.push l s.trail;
      List.iter (fun i -> s.c.on_assign <- s.c.on_assign + 1; s.tru.(i) <- s.tru.(i) + 1) s.occ.(idx l);
      let ok = ref true and units = ref [] in
      List.iter (fun i ->
          s.c.on_assign <- s.c.on_assign + 1;
          s.fls.(i) <- s.fls.(i) + 1;
          if s.tru.(i) = 0 then begin
            let len = Array.length s.cls.(i) in
            if s.fls.(i) = len then ok := false
            else if s.fls.(i) = len - 1 then
              units := Array.to_list s.cls.(i) |> List.filter (fun x -> value s x = 0) |> List.hd |> fun u -> u :: !units
          end) s.occ.(idx (-l));
      !ok && List.for_all (fun u -> assign s u) !units
    end
  let unassign_to s len =
    while Stack.length s.trail > len do
      let l = Stack.pop s.trail in
      s.value.(abs l) <- 0;
      List.iter (fun i -> s.c.on_backtrack <- s.c.on_backtrack + 1; s.tru.(i) <- s.tru.(i) - 1) s.occ.(idx l);
      List.iter (fun i -> s.c.on_backtrack <- s.c.on_backtrack + 1; s.fls.(i) <- s.fls.(i) - 1) s.occ.(idx (-l))
    done
end
 
(* Two watched literals: positions 0 and 1 of each clause. Only clauses
   watching a literal that has just become false are visited, and
   backtracking visits nothing. *)
module Watched : ENGINE = struct
  type t = { cls : int array array; watches : int list array; value : int array;
             trail : int array; mutable len : int; c : counts }
  let create n cls c =
    let watches = Array.make ((2 * n) + 2) [] in
    Array.iteri (fun i cl -> watches.(idx cl.(0)) <- i :: watches.(idx cl.(0));
                  watches.(idx cl.(1)) <- i :: watches.(idx cl.(1))) cls;
    { cls; watches; value = Array.make (n + 1) 0; trail = Array.make (n + 1) 0; len = 0; c }
  let value s l = let v = s.value.(abs l) in if l > 0 then v else -v
  let trail_length s = s.len
  let assign s l =
    if value s l = 1 then true else if value s l = -1 then false else begin
      let start = s.len in
      s.value.(abs l) <- (if l > 0 then 1 else -1); s.trail.(s.len) <- l; s.len <- s.len + 1;
      let q = ref start and ok = ref true in
      while !ok && !q < s.len do
        let f = - s.trail.(!q) in incr q;
        let pending = ref s.watches.(idx f) in
        s.watches.(idx f) <- [];
        while !pending <> [] do
          let i = List.hd !pending in pending := List.tl !pending;
          s.c.on_assign <- s.c.on_assign + 1;
          let c = s.cls.(i) in
          if c.(0) = f then (c.(0) <- c.(1); c.(1) <- f);
          let keep () = s.watches.(idx f) <- i :: s.watches.(idx f) in
          if value s c.(0) = 1 then keep ()                  (* satisfied: leave it *)
          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                (* move the watch *)
              c.(1) <- c.(!k); c.(!k) <- f; s.watches.(idx c.(1)) <- i :: s.watches.(idx c.(1))
            end else begin
              keep ();
              if value s c.(0) = -1 then (ok := false; s.watches.(idx f) <- !pending @ s.watches.(idx f); pending := [])
              else begin                                      (* unit: c.(0) is forced *)
                s.value.(abs c.(0)) <- (if c.(0) > 0 then 1 else -1);
                s.trail.(s.len) <- c.(0); s.len <- s.len + 1
              end
            end
          end
        done
      done;
      !ok
    end
  let unassign_to s len =
    for j = s.len - 1 downto len do s.value.(abs s.trail.(j)) <- 0 done;
    s.len <- len
end
 
(* The same DPLL search on top of either engine. *)
module Dpll (E : ENGINE) = struct
  let solve n cls =
    let c = { on_assign = 0; on_backtrack = 0 } in
    let e = E.create n cls c in
    let rec search () =
      let rec first v = if v > n then 0 else if E.value e v = 0 then v else first (v + 1) in
      let v = first 1 in
      v = 0 || begin
        let mark = E.trail_length e in
        (E.assign e v && search ()) || (E.unassign_to e mark; E.assign e (-v) && search ())
        || (E.unassign_to e mark; false)
      end in
    let r = search () in
    (r, c)
end

Running the same search with each engine on random 3-SAT formulas at the satisfiability threshold.

open Engines
module C = Dpll (Counters)
module W = Dpll (Watched)

Clause visits made while assigning and while backtracking.

  n  result   counters: assign  backtrack   watched: assign  backtrack
 40  SAT               10675      10165              2836          0
 60  UNSAT             86361      86361             21104          0
 80  SAT              621647     620627            151030          0
100  UNSAT          12551837   12551837           2564924          0

Both engines explore the same search tree. The counter scheme spends as much work undoing assignments as making them, and in total seven to ten times as many clause visits as the watched scheme, which does nothing on backtracking. The gap grows with clause length: learned clauses in CDCL solvers often have dozens or hundreds of literals, of which the watched scheme touches only the two watches unless they are hit^[1]^[6].

§ 03

Implementation

Most implementations keep the two watched literals in the first two positions of the clause, which is what the code above does; moving a watch swaps the new literal into position and pushes the clause onto the new literal's watch list^[3]. Several refinements are standard.

Blocking literals

Visiting a clause means loading it from memory, usually a cache miss. Chu, Harwood and Stuckey store with each watch-list entry one other literal of the clause, the blocking literal; if it is true, the clause is satisfied and need not be loaded at all^[4]. MiniSat and its successors adopted the technique.

Binary clauses

A clause of two literals is its own pair of watches and never moves them. Solvers therefore keep binary clauses in separate implication lists: when a literal becomes false, the other literal of each binary clause containing it is simply assigned^[7].

Where to look for a replacement

The scan for a new watch can start from the beginning of the clause or from where the last scan stopped. Gent analyzed the choices and showed that resuming the scan where the previous one stopped, wrapping around the clause, gives the best worst-case cost^[5].

§ 04

Other uses

The idea applies wherever a constraint can only propagate once all but a few of its variables are fixed. Constraint solvers such as Minion watch variables of general constraints^[9], and SMT solvers watch the atoms of theory lemmas in the same way as clauses. Pseudo-Boolean solvers generalize it to linear inequalities over Boolean variables, watching enough literals that their weights could still satisfy the constraint.

§ 05

History

Early DPLL implementations and GRASP detected unit clauses with counters of assigned literals per clause^[8]^[6]. Zhang's SATO of 1997 used head and tail pointers, which move inward from the ends of a clause as literals become false, and must be moved back on backtracking^[2]. The Chaff solver of Moskewicz, Madigan, Zhao, Zhang and Malik, published in 2001, replaced them with two watches that can be anywhere in the clause and need no restoration on backtracking; together with VSIDS it made Chaff an order of magnitude faster than earlier solvers^[1]. MiniSat's compact implementation of 2003 made the scheme standard^[3], and blocking literals were added in 2008^[4].