Implementing SAT in OCaml Part 2

2026-08-28 · 6 min

Part 1's dpll hits pigeonhole instances of size six and above with no way to remember that a whole family of branches is dead for the same reason - it explores each one from scratch. CDCL fixes this by analyzing every conflict, deriving a new clause that explains it, and jumping straight back to the decision level that clause is actually about, instead of undoing one choice at a time.

§ 01

A record-based solver state

Clauses now carry a learnt flag, since learned clauses are added at runtime rather than only at parse time. lib/cdcl.ml, alongside Part 1's sat.ml.

(* lib/cdcl.ml *)
open Sat_lib
 
type clause = { lits : lit array; learnt : bool }
 
type solver = {
  n : int;                          (* variables are 1..n *)
  mutable clauses : clause list;
  value : bool option array;        (* index 1..n *)
  level : int array;                (* index 1..n, -1 if unassigned *)
  reason : clause option array;     (* index 1..n; None = decision or unassigned *)
  mutable trail : lit list;          (* most recently assigned literal first *)
  mutable dlevel : int;
}

Construction, turning Part 1's plain int list list formula into the richer clause records.

let make_solver (n : int) (f : formula) : solver =
  {
    n;
    clauses = List.map (fun lits -> { lits = Array.of_list lits; learnt = false }) f;
    value = Array.make (n + 1) None;
    level = Array.make (n + 1) (-1);
    reason = Array.make (n + 1) None;
    trail = [];
    dlevel = 0;
  }

Reading a literal's value directly off the arrays rather than a Hashtbl - the fixed 1..n range makes an array the right structure now.

let lit_value (s : solver) (l : lit) : bool option =
  match s.value.(var l) with
  | None -> None
  | Some b -> Some (if l > 0 then b else not b)
 
let enqueue (s : solver) (l : lit) (reason : clause option) : unit =
  s.value.(var l) <- Some (l > 0);
  s.level.(var l) <- s.dlevel;
  s.reason.(var l) <- reason;
  s.trail <- l :: s.trail

§ 02

Propagation, returning the conflicting clause

Same idea as Part 1's unit_propagate, but now it reports which clause conflicted rather than just a bool - conflict analysis needs that clause. No watched literals here: every pass rescans every clause, which is the honest tradeoff of this post being about correctness of the learning algorithm rather than a production-speed implementation.

let propagate (s : solver) : clause option =
  let conflict = ref None in
  let changed = ref true in
  while !changed && !conflict = None do
    changed := false;
    List.iter
      (fun c ->
        if !conflict = None then begin
          let unassigned = ref [] in
          let sat = ref false in
          Array.iter
            (fun l ->
              match lit_value s l with
              | Some true -> sat := true
              | Some false -> ()
              | None -> unassigned := l :: !unassigned)
            c.lits;
          if not !sat then
            match !unassigned with
            | [] -> conflict := Some c
            | [ l ] -> enqueue s l (Some c); changed := true
            | _ -> ()
        end)
      s.clauses
  done;
  !conflict

§ 03

First-UIP conflict analysis

On a conflict, walk backward through the trail, resolving the conflicting clause against the reason for each literal at the current decision level, until exactly one literal from the current level remains - the first unique implication point. Everything else collected along the way, from earlier levels, becomes the rest of the learned clause.

seen marks which variables have already been folded into the resolution; counter tracks how many literals from the current decision level are still unresolved. The loop terminates exactly when counter reaches zero, which is guaranteed since a decision literal always has no reason, and a decision literal at the current level is always eventually reached.

let analyze (s : solver) (conflict : clause) : lit list * int =
  let seen = Array.make (s.n + 1) false in
  let learnt = ref [] in
  let counter = ref 0 in
  let p = ref None in
  let reason_lits = ref conflict.lits in
  let trail = ref s.trail in
  let continue_ = ref true in
  while !continue_ do
    Array.iter
      (fun q ->
        let is_p = match !p with Some pl -> q = pl | None -> false in
        if not is_p then begin
          let v = var q in
          if not seen.(v) then begin
            seen.(v) <- true;
            if s.level.(v) = s.dlevel then incr counter
            else if s.level.(v) > 0 then learnt := q :: !learnt
            (* level 0 literals are permanent facts, omitted from the learned clause *)
          end
        end)
      !reason_lits;
    let rec pop t =
      match t with
      | [] -> failwith "analyze: exhausted the trail before reaching a UIP"
      | l :: rest -> if seen.(var l) then (l, rest) else pop rest
    in
    let pl, rest = pop !trail in
    trail := rest;
    seen.(var pl) <- false;
    decr counter;
    if !counter = 0 then begin
      p := Some pl;
      continue_ := false
    end else begin
      p := Some pl;
      reason_lits :=
        (match s.reason.(var pl) with
         | Some c -> c.lits
         | None -> failwith "analyze: reached a decision literal before counter hit zero")
    end
  done;
  let uip = Option.get !p in
  let out_learnt = neg uip :: !learnt in
  let bt_level =
    List.fold_left
      (fun acc l -> if l = neg uip then acc else max acc s.level.(var l))
      0 out_learnt
  in
  (out_learnt, bt_level)

Tracing analyze by hand: three decisions x1, x2, x3 (levels 1, 2, 3), where x3's propagation eventually falsifies a clause (-x1 -x2 -x3). Resolving that clause against the reasons for x2 and x3 in turn, both at level 3 or below the point where only x1's negation remains from level 1, yields the learned clause (-x1) at backtrack level 0 - a unit clause that, once added, immediately forces x1 = false everywhere, permanently.

conflict clause: (-1 -2 -3)
resolve away -3 (decided at level 3, its own reason is None - it IS the UIP
  at level 3, so counter hits 0 immediately for this toy trail shape)
learnt = [-1]   bt_level = 0
-> backtrack to level 0, enqueue -1 as a unit fact, never revisit x1=true again

§ 04

Backtracking and the main loop

Undo every assignment made after the target level, restoring None/−1/None on the way - and update dlevel itself.

let backtrack (s : solver) (level : int) : unit =
  s.trail <-
    List.filter
      (fun l ->
        if s.level.(var l) > level then begin
          s.value.(var l) <- None;
          s.level.(var l) <- -1;
          s.reason.(var l) <- None;
          false
        end else true)
      s.trail;
  s.dlevel <- level

The simplest possible decision heuristic: the lowest-numbered unassigned variable, always tried true first. Real solvers use activity-based heuristics like VSIDS; that is a speed concern, not a correctness one, so it is left out here.

let pick_branch (s : solver) : int option =
  let rec go v = if v > s.n then None
    else if s.value.(v) = None then Some v
    else go (v + 1)
  in
  go 1

The CDCL loop itself. A conflict at decision level 0 is unconditionally UNSAT - there is nothing left to backtrack past. Otherwise: analyze, learn, backjump, and enqueue the asserting literal - the head of out_learnt, which is always the UIP's negation and is guaranteed to be unit (hence forced true) at the new, lower decision level.

let rec cdcl (s : solver) : bool option array option =
  match propagate s with
  | Some conflict ->
    if s.dlevel = 0 then None
    else begin
      let learnt, bt_level = analyze s conflict in
      let learnt_clause = { lits = Array.of_list learnt; learnt = true } in
      s.clauses <- learnt_clause :: s.clauses;
      backtrack s bt_level;
      let asserting = List.hd learnt in
      enqueue s asserting (Some learnt_clause);
      cdcl s
    end
  | None ->
    (match pick_branch s with
     | None -> Some (Array.copy s.value)
     | Some v ->
       s.dlevel <- s.dlevel + 1;
       enqueue s v None;
       cdcl s)
 
let solve (n : int) (f : formula) : bool option array option =
  cdcl (make_solver n f)

§ 05

Checking it against Part 1

Same result on the small example from Part 1, now returning a bool option array indexed by variable rather than a Hashtbl.

# solve 3 Sat_lib.example;;
- : bool option array option =
Some [|None; Some true; Some false; Some true|]
(* index 0 unused; x1=true, x2=false, x3=true *)

A tiny sanity checker, run against every clause of the original formula - useful for every solver built in this series from here on, since a solver that claims SAT owes you a model that actually checks out.

let check_model (f : formula) (m : bool option array) : bool =
  List.for_all
    (fun c ->
      List.exists
        (fun l ->
          match m.(var l) with
          | Some b -> b = (l > 0)
          | None -> false)
        c)
    f

§ 06

Pigeonhole, revisited

The six-into-five pigeonhole instance that made Part 1's plain DPLL noticeably slow now returns in a fraction of the time - every dead branch caused by the same underlying counting argument collapses into a small number of learned clauses instead of being rediscovered from scratch each time.

# let f, n = Sat_lib.pigeonhole 6 5, (6 * 5) in
  solve n f;;
- : bool option array option = None

Counting learned clauses gives a rough sense of how much work non-chronological backtracking is actually saving on a given instance.

let solve_verbose (n : int) (f : formula) =
  let s = make_solver n f in
  let result = cdcl s in
  let learnt_count = List.length (List.filter (fun c -> c.learnt) s.clauses) in
  Printf.printf "learned %d clauses\n" learnt_count;
  result

§ 07

What is still missing

Named honestly, in the order they matter for speed rather than correctness: two-watched-literal propagation (this post rescans every clause on every propagation step, which is the single biggest performance gap versus a real solver); a decision heuristic with memory, such as VSIDS, instead of always picking the lowest free variable; clause deletion, since learned clauses accumulate without bound here; and restarts. None of the four change whether the answer is right - only how long it takes to get there.

watched literals    O(1) amortized propagation instead of O(clauses) per step
VSIDS               branch on variables that have been in recent conflicts
clause deletion      periodically drop low-activity learned clauses
restarts             abandon a long unlucky branch and re-decide from level 0

← older

Introduction to odoc

2026-08-23

newer →

Profiling GHC Programs

2026-08-30