Watched literals

also: two-watched-literal, watch list

Two literals per clause are watched, with the invariant that neither is false unless the clause is already unit or falsified. A clause is only inspected when one of its watches becomes false, so propagation costs what it actually propagates rather than a rescan of the database, and backtracking costs nothing at all.

Unit propagation is where a SAT solver spends most of its time, and the naive implementation rescans every clause on every assignment. The observation that fixes it: a clause can only become unit or falsified when one of its literals becomes false, and it is enough to watch two.

Keep two watched literals per clause, maintaining the invariant that neither is false unless the clause is already unit or falsified. When a watch becomes false, look for a replacement among the other literals. If one exists, move the watch and the clause is not yet interesting. If none exists, the clause is unit on the surviving watch, or falsified if that one is false too.

The rescue step, which is the whole scheme. Compiled with ocamlopt 4.14.1.

let rescue (c : clause) =
  let other = if value c.lits.(c.w0) = Some false then c.w1 else c.w0 in
  let falsified = if other = c.w0 then c.w1 else c.w0 in
  if value c.lits.(other) = Some true then `Ok
  else begin
    let found = ref (-1) in
    for i = 0 to Array.length c.lits - 1 do
      if !found < 0 && i <> other && i <> falsified
         && value c.lits.(i) <> Some false then found := i
    done;
    if !found >= 0 then begin
      if falsified = c.w0 then c.w0 <- !found else c.w1 <- !found;
      `Ok
    end
    else if value c.lits.(other) = None then `Unit c.lits.(other)
    else `Conflict
  end

Clause (x1 or x2 or x3) watching x1 and x2, with the three literals falsified in turn.

x1 := false   ->  watch moved to index 2 (literal 3)
x2 := false   ->  unit: 3 must be true
x3 := false   ->  conflict: every literal false

The property that makes it pay is what happens on backtracking: nothing. A watch that was valid at a deeper decision level is still valid at a shallower one, because unassigning literals only ever makes the invariant easier to satisfy. So undoing a decision costs exactly the trail pops, and never a pass over the clause database.