Unit propagation

also: bcp, boolean constraint propagation

The inference rule that does most of the work in a SAT solver: if every literal of a clause is false except one unassigned literal, that literal must be true. Applying it to fixpoint after each decision is where solvers spend the bulk of their time, which is why the data structure that finds unit clauses is the thing worth optimizing.

The one inference rule that does most of the work. If every literal in a clause is false except one, which is unassigned, then that literal must be true in any satisfying extension:

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

Applying it to fixpoint after every decision is where a solver spends most of its time, typically far more than in the search itself. That is why the data structure that finds unit clauses, rather than the branching heuristic, is the thing worth optimising.

The rule directly, as a fold over the clause list. Compiled with ocamlopt 4.14.1.

let rec propagate cs a =
  let step = List.fold_left (fun acc c ->
    match acc with
    | None -> None
    | Some (a, changed) ->
      let unassigned = List.filter (fun l -> value a l = None) c in
      if List.exists (fun l -> value a l = Some true) c then Some (a, changed)
      else match unassigned with
        | [] -> None                                (* conflict *)
        | [ l ] -> Some ((abs l, l > 0) :: a, true) (* unit *)
        | _ -> Some (a, changed)) (Some (a, false)) cs
  in
  match step with
  | None -> None
  | Some (a, false) -> Some a
  | Some (a, true) -> propagate cs a

Scanning every clause on every assignment, as above, is quadratic in the obvious way. Real solvers keep two watched literals per clause and only inspect a clause when one of its two watches becomes false, which makes the cost proportional to the propagations that actually happen rather than to the size of the database. Backtracking then costs nothing, because the watches are still valid.