First-UIP conflict analysis

In a conflict-driven clause-learning SAT solver, conflict analysis turns each conflict into a new clause that records why the conflict happened^[1]. When unit propagation falsifies a clause, every literal of that clause is false because of earlier decisions and propagations, which are recorded in an implication graph: each propagated literal points back to the literals that forced it through its reason clause. The analysis resolves the conflicting clause with the reasons of its literals, working backwards along the trail of assignments, until the clause contains exactly one literal assigned at the current decision level. That literal is the first unique implication point, first UIP. The derived clause is added to the formula as a learned clause, and the solver backtracks to the second-highest decision level among its literals, where the learned clause becomes unit and forces the UIP's negation. First-UIP learning was identified as the most effective scheme by Zhang, Madigan, Moskewicz and Malik in 2001^[2], and is used by essentially all CDCL solvers.

§ 01

The implication graph

During search, each assigned literal carries a decision level, the number of decisions made when it was assigned, and a reason: nothing for a decision, or the clause that became unit and forced it. The implication graph has a node for each assigned literal and an edge from each false literal of a reason clause to the literal it forced; a conflict adds a node with edges from the literals of the falsified clause^[1]^[7].

Consider the clauses

ω_{1} ω_{3} ω_{5} = \neg x_{1} \lor x_{2} = \neg x_{2} \lor \neg x_{3} \lor x_{4} = \neg x_{4} \lor x_{6} \lor x_{11} ω_{2} ω_{4} ω_{6} = \neg x_{1} \lor x_{3} \lor x_{9} = \neg x_{4} \lor x_{5} \lor x_{10} = \neg x_{5} \lor \neg x_{6}

with $x_{9}$ false at level 1, $x_{10}$ and $x_{11}$ false at level 3, and the decision $x_{1} = 1$ at level 6. Propagation sets $x_{2}$ through $x_{6}$ true, and $ω_{6}$ becomes false.

The implication graph at the conflict. Every path from the decision x₁ to the conflict passes through x₄, which is therefore a unique implication point; x₁ itself is another. The dashed cut separates the conflict side from the rest; the literals on the other side with edges crossing it, x₄, x₁₀ and x₁₁, give the learned clause (¬x₄ ∨ x₁₀ ∨ x₁₁).

§ 02

Deriving the clause

A unique implication point is a node of the current level that lies on every path from the level's decision to the conflict. The decision is always one; the first UIP is the one closest to the conflict. Any cut of the graph that separates the conflict from the decisions gives a learned clause, the disjunction of the negations of the literals with an edge crossing the cut. Every assignment that makes those literals true leads by propagation to the same conflict, so the clause is implied by the formula. Choosing the cut just after the first UIP gives the first-UIP clause^[2].

Solvers compute it by resolution rather than by graph search. Starting from the conflicting clause, they repeatedly pick the literal of the current level assigned last, resolve with its reason clause, and stop when one literal of the current level remains. Each step is a resolution step, so the learned clause is derivable from the formula by a resolution proof^[3].

Conflict analysis on an explicit trail, printing each resolution step.

(* Conflict analysis on an explicit trail. Each entry is a literal made
   true, its decision level, and the clause that implied it (None for a
   decision). *)
type entry = { lit : int; level : int; reason : int list option }
 
let show_clause c = "(" ^ String.concat " ∨ " (List.map (fun l -> (if l < 0 then "¬x" else "x") ^ string_of_int (abs l)) c) ^ ")"
 
(* Pad to a width in characters, not bytes. *)
let pad n s =
  let chars = ref 0 in
  String.iter (fun ch -> if Char.code ch land 0xC0 <> 0x80 then incr chars) s;
  s ^ String.make (max 0 (n - !chars)) ' '
 
(* Resolve on variable v: the clauses contain v with opposite signs. *)
let resolve a b v =
  List.sort_uniq compare (List.filter (fun l -> abs l <> v) (a @ b))
 
(* Walk the trail backwards, resolving the conflicting clause with the
   reason of each current-level literal it contains, and stop as soon as
   the clause has exactly one literal of the current level (a UIP), or
   continue to the decision if stop_at_first is false. *)
let analyze ?(stop_at_first = true) trail conflict =
  let level_of v = (List.find (fun e -> abs e.lit = v) trail).level in
  let current = (List.hd (List.rev trail)).level in
  let at_current c = List.filter (fun l -> level_of (abs l) = current) c in
  let rec go c = function
    | [] -> c
    | e :: earlier ->
      let v = abs e.lit in
      let done_ = List.length (at_current c) = 1 && stop_at_first in
      if done_ || not (List.mem (-e.lit) c) then (if done_ then c else go c earlier)
      else match e.reason with
        | None -> c                                         (* reached the decision *)
        | Some r ->
          let c' = resolve c r v in
          Printf.printf "  resolve on x%-2d with %s -> %s\n" v (pad 18 (show_clause r)) (show_clause c');
          go c' earlier
  in
  go conflict (List.rev trail)

The example above, stopping at the first UIP and continuing to the decision.

open Analysis
 
(* The clauses of the example, with x9, x10, x11 set false at lower
   levels and x1 decided true at level 6. *)
let w1 = [ -1; 2 ] and w2 = [ -1; 3; 9 ] and w3 = [ -2; -3; 4 ]
and w4 = [ -4; 5; 10 ] and w5 = [ -4; 6; 11 ] and w6 = [ -5; -6 ]
 
let trail = [
  { lit = -9; level = 1; reason = None };
  { lit = -10; level = 3; reason = None };
  { lit = -11; level = 3; reason = None };
  { lit = 1; level = 6; reason = None };
  { lit = 2; level = 6; reason = Some w1 };
  { lit = 3; level = 6; reason = Some w2 };
  { lit = 4; level = 6; reason = Some w3 };
  { lit = 5; level = 6; reason = Some w4 };
  { lit = 6; level = 6; reason = Some w5 } ]

Running it.

conflict in (¬x5 ∨ ¬x6)
first UIP:
  resolve on x6  with (¬x4 ∨ x6 ∨ x11)   -> (¬x5 ∨ ¬x4 ∨ x11)
  resolve on x5  with (¬x4 ∨ x5 ∨ x10)   -> (¬x4 ∨ x10 ∨ x11)
  learned (¬x4 ∨ x10 ∨ x11): jump back to level 3, where it forces ¬x4
resolving back to the decision:
  resolve on x6  with (¬x4 ∨ x6 ∨ x11)   -> (¬x5 ∨ ¬x4 ∨ x11)
  resolve on x5  with (¬x4 ∨ x5 ∨ x10)   -> (¬x4 ∨ x10 ∨ x11)
  resolve on x4  with (¬x2 ∨ ¬x3 ∨ x4)   -> (¬x3 ∨ ¬x2 ∨ x10 ∨ x11)
  resolve on x3  with (¬x1 ∨ x3 ∨ x9)    -> (¬x2 ∨ ¬x1 ∨ x9 ∨ x10 ∨ x11)
  resolve on x2  with (¬x1 ∨ x2)         -> (¬x1 ∨ x9 ∨ x10 ∨ x11)
  learned (¬x1 ∨ x9 ∨ x10 ∨ x11)

§ 03

Backjumping

The learned clause contains exactly one literal of the current level, $\neg x_{4}$ , and its other literals were assigned at earlier levels. The solver undoes assignments back to the highest of those levels, here level 3, rather than just to level 5. At level 3, $x_{10}$ and $x_{11}$ are still false, so the learned clause is unit and forces $x_{4} = 0$ immediately. This is non-chronological backjumping: decisions at levels 4 and 5, which had nothing to do with the conflict, are discarded, and the implication $\neg x_{4}$ is placed as early in the search as its justification allows^[1]. Because the clause is asserting, with a single literal at the conflict level, the solver never needs to flip a decision explicitly as DPLL does.

§ 04

Why the first UIP

Any UIP gives an asserting clause, and so do cuts containing several literals of the current level if the solver is prepared to handle them. Zhang and co-authors compared a range of schemes in 2001, including learning a clause of decisions only and learning a clause for every UIP, and found the first UIP best on their benchmarks: its clause is usually short, it is closest to the conflict and so most specific, and it backjumps at least as far as the others^[2].

First-UIP learning against resolving all the way to the decision at the conflict level, in the same solver.

(* First-UIP learning against resolving back to the decision, the last
   UIP, in the same solver, with the average learned clause length. *)
let run cfg f =
  let total = ref 0 and n = ref 0 in
  let setup (s : Cdcl.t) = s.on_learn <- (fun c -> total := !total + Array.length c; incr n) in
  let r, st = Cdcl.solve ~cfg ~setup f in
  (r, st.Cdcl.conflicts, float !total /. float (max 1 !n))

Conflicts and average learned clause length.

instance                 first UIP: conflicts, length last UIP: conflicts, length
random 3-SAT, 80 vars               169     6.0               236     7.0
random 3-SAT, 100 vars              442     7.6               590     8.1
random 3-SAT, 120 vars             1432     9.4              1576    10.4
pigeonhole, 7 in 6                  758    13.2               889    14.6
pigeonhole, 8 in 7                 4164    19.9              6129    21.6

On these formulas the first-UIP clauses are shorter and the solver needs 10 to 30% fewer conflicts. The difference is larger on structured industrial formulas, where implication chains are long.

§ 05

Refinements

Minimization

A literal of the learned clause is redundant if its negation is implied by the negations of the other literals through reason clauses. Removing such literals, by checking reasons recursively, shortens learned clauses by roughly 30% on typical industrial problems^[4].

Clause quality

Learned clauses accumulate, and solvers periodically delete many of them. Audemard and Simon measured the quality of a learned clause by its literal block distance (LBD), the number of different decision levels among its literals, and found that clauses of low LBD, especially those with LBD 2, called glue clauses, are the most useful to keep^[6].

§ 06

History

Explaining a failure by the assumptions it depended on, and backtracking to the relevant one, goes back to dependency-directed backtracking in Stallman and Sussman's circuit analysis program of 1977^[9]. Marques-Silva and Sakallah brought the idea to SAT with GRASP, first presented in 1996, which introduced the implication graph, unique implication points, learned clauses and non-chronological backtracking^[1]. Bayardo and Schrag's rel_sat of 1997 combined learning with look-back techniques from constraint satisfaction^[8]. Zhang, Madigan, Moskewicz and Malik's comparison of learning schemes in 2001 established the first UIP^[2], MiniSat's implementation became the reference^[5], and clause minimization and LBD followed in 2009^[4]^[6]. Beame, Kautz and Sabharwal related the learned clauses to resolution proofs^[3].