CDCL

Conflict-driven clause learning (CDCL) is the search algorithm used by practically every complete SAT solver^[13]. It keeps the structure of DPLL: assign variables by decisions, propagate their consequences by unit propagation, and backtrack on conflict. What it adds is learning. A conflict is not just a dead end but a proof that some combination of assignments cannot be extended to a model. CDCL extracts that proof as a new clause by conflict analysis, adds it to the clause database, and jumps back to the earliest decision level at which the new clause forces a literal, skipping decisions that had nothing to do with the conflict. The learned clause stops the same conflict from happening again anywhere else in the search. GRASP introduced the method in 1996^[1]; Chaff added watched literals and the VSIDS heuristic in 2001^[2], and MiniSat made the design standard^[7].

§ 01

The loop

The main loop of a CDCL solver. Unit propagation runs after every decision and every learned clause; a conflict leads to analysis, learning and a backjump, after which the learned clause itself propagates. The solver stops with a model when every variable is assigned, and proves unsatisfiability when a conflict occurs with no decisions left to undo.

The solver keeps a trail of assigned literals, each with its decision level and the clause that forced it. Each iteration propagates. If no clause is falsified, it makes a decision on an unassigned variable, opening a new level, or reports a model if none is left. If a clause is falsified, it analyzes the conflict, learns a clause with exactly one literal at the current level, undoes the trail back to the second-highest level among the clause's literals, and lets the learned clause propagate there^[1]^[13]. A conflict at level 0 depends on no decision at all, so the formula is unsatisfiable.

The main loop of a CDCL solver with watched literals, first-UIP learning, VSIDS and Luby restarts; the helper functions are omitted.

let solve ?cfg ?(setup = ignore) (f : Cnf.cnf) =
  let s = create ?cfg f in
  setup s;
  let ok = ref true in
  List.iter (fun c ->
      let c = List.sort_uniq compare c in
      if List.exists (fun l -> List.mem (-l) c) c then ()          (* tautology *)
      else match c with
        | [] -> ok := false
        | [ l ] -> if lit_value s l = -1 then ok := false else if lit_value s l = 0 then assign s l (-1)
        | _ -> ignore (add_clause_raw s (Array.of_list c))) f.clauses;
  let result = ref None in
  if not !ok then result := Some Unsat;
  let restart_no = ref 1 and budget = ref 100 in
  while !result = None do
    let confl = propagate s in
    if confl >= 0 then begin
      s.st.conflicts <- s.st.conflicts + 1; decr budget; s.on_conflict ();
      if s.dl = 0 then result := Some Unsat
      else if s.st.conflicts > s.cfg.limit then result := Some Unknown
      else if s.cfg.learn then begin
        let learnt, back = analyze s confl in
        s.on_learn learnt;
        cancel_until s back;
        s.inc <- s.inc /. 0.95;                    (* decay: newer bumps count more *)
        if Array.length learnt = 1 then assign s learnt.(0) (-1)
        else begin
          s.st.learned <- s.st.learned + 1;
          assign s learnt.(0) (add_clause_raw s learnt)
        end
      end else begin
        (* DPLL: undo the latest decision and assert its negation one level
           down, where it stays until that level is undone in turn *)
        let d = s.trail.(s.lim.(s.dl - 1)) in
        cancel_until s (s.dl - 1);
        assign s (-d) (-2)
      end
    end else if s.cfg.restarts && s.cfg.learn && !budget <= 0 then begin
      cancel_until s 0; incr restart_no; budget := 100 * luby !restart_no
    end else begin
      let v = pick s in
      if v = 0 then result := Some (Sat (Array.init (s.n + 1) (fun v -> s.value.(v) = 1)))
      else begin
        s.st.decisions <- s.st.decisions + 1;
        s.lim.(s.dl) <- s.len; s.dl <- s.dl + 1;
        assign s (if s.phase.(v) then v else -v) (-1)
      end
    end
  done;
  (Option.get !result, s.st)

§ 02

An example

Take the five clauses

c_{1} c_{3} c_{5} = \neg x_{1} \lor x_{4} = \neg x_{5} \lor x_{6} = \neg x_{6} \lor \neg x_{7} c_{2} c_{4} = \neg x_{2} \lor \neg x_{3} \lor x_{5} = \neg x_{4} \lor \neg x_{5} \lor x_{7}

Deciding $x_{1}$ at level 1 implies $x_{4}$ through $c_{1}$ . Deciding $x_{2}$ at level 2 implies nothing. Deciding $x_{3}$ at level 3 implies $x_{5}$ through $c_{2}$ , then $x_{6}$ and $x_{7}$ , and $c_{5}$ is falsified.

The implication graph at the conflict. Shaded nodes are decisions, the rest are implied by the clause on their incoming edges; @n is the decision level.

Conflict analysis resolves $c_{5}$ with the reasons for $x_{6}$ and $x_{7}$ and learns $\neg x_{4} \lor \neg x_{5}$ . Its literals are at levels 1 and 3, so the solver backjumps from level 3 directly to level 1, undoing the decision on $x_{2}$ along the way, and at level 1 the learned clause is unit and sets $x_{5}$ to false. It mentions neither $x_{2}$ nor $x_{3}$ : the conflict follows from $x_{4}$ and $x_{5}$ alone, whatever made $x_{5}$ true.

§ 03

Components

Learning, backjumping and branching are the core; a practical solver adds several further techniques^[13].

Restarts

From time to time the solver undoes all decisions and starts the search again, keeping its learned clauses, activity scores and saved phases. Restarts guard against runs that are stuck in an unproductive part of the search space, whose running times on randomized solvers are heavy-tailed^[9]. MiniSat and its successors space restarts by the Luby sequence 1, 1, 2, 1, 1, 2, 4, …, multiplied by a base interval, which is optimal for restarting a Las Vegas algorithm with unknown run-time distribution^[8]^[7]. Because of phase saving, a restart usually rebuilds a similar assignment quickly, so restarts can be frequent.

Clause deletion

Learned clauses slow propagation and fill memory, so solvers delete most of them periodically. MiniSat kept clauses that had recently taken part in conflicts^[7]; Glucose introduced the literal block distance, the number of distinct decision levels in a clause, and keeps clauses with small LBD indefinitely^[10].

Preprocessing and inprocessing

Before and during search, solvers simplify the formula: bounded variable elimination resolves away variables when this does not increase the number of clauses, and subsumption, blocked clause elimination and equivalent-literal substitution remove redundancy^[11].

Incremental solving

Many applications solve a sequence of related formulas. MiniSat's interface allows clauses to be added between calls and each call to be made under assumptions, literals that are treated as decisions at the lowest levels; learned clauses remain valid across calls because they are implied by the clauses alone^[12]. Bounded model checking and SMT solvers depend on this.

§ 04

The contribution of each part

Switching features off one at a time, on random 3-SAT, graph colouring and pigeonhole formulas, all unsatisfiable.

(* Switching the parts of a CDCL solver off one at a time. *)
let colouring ~vertices ~edges ~colours =
  let x v c = (v * colours) + c + 1 in
  Cnf.of_clauses
    (List.init vertices (fun v -> List.init colours (x v))
     @ List.concat_map (fun (u, v) -> List.init colours (fun c -> [ - (x u c); - (x v c) ])) edges)
let random_graph n m =
  let rec go acc = if List.length acc = m then acc else
      let u = Random.int n and v = Random.int n in
      if u = v || List.mem (min u v, max u v) acc then go acc else go ((min u v, max u v) :: acc) in
  go []

Conflicts needed, with a limit of 300,000.

conflicts                3-SAT 100     3-SAT 130  colouring 70     7 pigeons
full                           371           795           358           758
no restarts                    470           893           376           847
no VSIDS                      2102          7798           888           130
no learning (DPLL)           41903      > 300000      > 300000          3246
result                       UNSAT         UNSAT         UNSAT         UNSAT

Learning is the decisive ingredient: without it, the solver becomes DPLL, and two of the four formulas are out of reach within the limit. The branching heuristic matters by factors of two to ten, except on the pigeonhole formula, where the fixed variable order happens to follow its structure. Restarts matter little on these small formulas; their benefit shows on large industrial instances.

§ 05

Proof complexity

Each learned clause is derived from the formula by resolution, so a CDCL run on an unsatisfiable formula is a resolution refutation. The converse also holds: CDCL with restarts, and with the right decisions, polynomially simulates general resolution^[3]^[4], whereas DPLL corresponds to tree-like resolution^[5], which is exponentially weaker on some formulas^[6]. Formulas that are hard for resolution, such as the pigeonhole formulas, are therefore hard for CDCL as well.

§ 06

History

Marques-Silva and Sakallah introduced conflict analysis, clause learning and non-chronological backtracking in GRASP, presented in 1996 and published in 1999^[1]; Bayardo and Schrag's rel_sat of 1997 used related learning^[14]. Chaff, from Princeton in 2001, combined first-UIP learning with watched literals and VSIDS and was an order of magnitude faster than earlier solvers^[2]. Eén and Sörensson's MiniSat, first released in 2003, distilled the design into a small, readable C++ program and became the base of many later solvers^[7]. The following decade added clause minimization, LBD-based deletion, phase saving, inprocessing and rapid restarts^[10]^[11]; the theoretical explanation of CDCL's power as a resolution engine came in 2004 and 2011^[5]^[3]^[4].