Implementing SAT in OCaml Part 3

2026-09-04 · 6 min

SMT stands for satisfiability modulo theories: the boolean skeleton is decided the same way Part 2 already does it, but individual boolean variables now stand for atoms in some theory - equalities, linear inequalities - rather than being meaningless propositional letters. The DPLL(T) architecture bolts a theory solver onto CDCL with almost no change to CDCL itself, which is the part worth seeing concretely.

§ 01

Refactoring Part 2: one conflict handler

Part 2's cdcl special-cased boolean conflicts inline. Pulling that into its own function is what makes plugging in theory conflicts later a non-event - both kinds of conflict end up calling exactly this.

(* lib/dpll_t.ml *)
open Sat_lib
open Cdcl
 
(* returns None on a level-0 conflict (UNSAT), Some () once the
   learned clause is added, backjumped to, and its asserting
   literal enqueued. *)
let handle_conflict (s : solver) (conflict : clause) : unit option =
  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);
    Some ()
  end

§ 02

The theory interface

An atom is whatever the theory reasons about - here, equalities and disequalities between term ids. check takes the atoms currently true under the boolean assignment and either confirms consistency or names a subset that cannot all hold together.

type term = int
 
type atom =
  | Eq of term * term
  | Neq of term * term
 
module type THEORY = sig
  val check : atom list -> atom list option
  (* None = consistent. Some conflicting = this subset cannot all be true *)
end

§ 03

A real, if small, theory: equality via union-find

Path-compressed, union-by-rank union-find - nothing SMT-specific about it yet, just the standard structure.

(* lib/union_find.ml *)
type t = { parent : int array; rank : int array }
 
let create (n : int) : t =
  { parent = Array.init n (fun i -> i); rank = Array.make n 0 }
 
let rec find (uf : t) (x : int) : int =
  if uf.parent.(x) = x then x
  else begin
    let r = find uf uf.parent.(x) in
    uf.parent.(x) <- r;
    r
  end
 
let union (uf : t) (x : int) (y : int) : unit =
  let rx = find uf x and ry = find uf y in
  if rx <> ry then
    if uf.rank.(rx) < uf.rank.(ry) then uf.parent.(rx) <- ry
    else if uf.rank.(rx) > uf.rank.(ry) then uf.parent.(ry) <- rx
    else begin
      uf.parent.(ry) <- rx;
      uf.rank.(rx) <- uf.rank.(rx) + 1
    end

check: union every Eq atom first, then look for a Neq whose two sides ended up in the same class - a direct contradiction. num_terms is threaded through since union-find needs to know its universe size up front.

(* lib/eq_theory.ml *)
open Union_find
 
let check (num_terms : int) (atoms : atom list) : atom list option =
  let uf = create num_terms in
  let eqs = List.filter_map (function Eq (a, b) -> Some (a, b) | Neq _ -> None) atoms in
  List.iter (fun (a, b) -> union uf a b) eqs;
  let violated =
    List.find_opt
      (function Neq (a, b) -> find uf a = find uf b | Eq _ -> false)
      atoms
  in
  match violated with
  | None -> None
  | Some bad_neq ->
    Some (List.filter (function Eq _ -> true | Neq _ -> false) atoms @ [ bad_neq ])

The conflict returned here is every currently-true equality plus the violated disequality - sound (that exact combination really is contradictory), but not minimal: a real congruence closure tracks which specific chain of equalities merged the two terms and returns only that chain. Returning everything is honest scope-cutting, not a bug - the SAT layer above still learns a correct clause from it, just a less general one than the best possible explanation would give.

Transitivity failing directly: x=y, y=z, x<>z can never all hold. check catches it because union merges x, y, and z into one class before the Neq is examined.

# check 3 [ Eq (0, 1); Eq (1, 2); Neq (0, 2) ];;
- : atom list option =
Some [Eq (0, 1); Eq (1, 2); Neq (0, 2)]
 
# check 3 [ Eq (0, 1); Neq (1, 2) ];;
- : atom list option = None   (* consistent: 0 and 2 were never forced equal *)

§ 04

Wiring atoms to boolean variables

Every distinct atom in the problem gets exactly one fresh boolean variable - a bidirectional table is all that connects the two layers.

(* lib/atomize.ml *)
open Dpll_t
 
type atomization = {
  atom_of_var : (int, atom) Hashtbl.t;
  var_of_atom : (atom, int) Hashtbl.t;
  num_terms : int;
}
 
let make (num_terms : int) (atoms : atom list) : atomization =
  let atom_of_var = Hashtbl.create 64 in
  let var_of_atom = Hashtbl.create 64 in
  List.iteri
    (fun i atom ->
      let v = i + 1 in
      Hashtbl.replace atom_of_var v atom;
      Hashtbl.replace var_of_atom atom v)
    (List.sort_uniq compare atoms);
  { atom_of_var; var_of_atom; num_terms }

Reading off the currently-true atoms from a fully assigned boolean state - exactly the variables whose value is true, mapped back through the table.

let true_atoms (s : Cdcl.solver) (az : atomization) : atom list =
  List.filter_map
    (fun v ->
      if s.Cdcl.value.(v) = Some true then Hashtbl.find_opt az.atom_of_var v
      else None)
    (List.init s.Cdcl.n (fun i -> i + 1))

Turning a theory-conflicting subset of atoms into a blocking clause - every one of them was true, so the clause forbidding that exact combination is the disjunction of their negations.

let theory_clause (az : atomization) (conflicting : atom list) : Cdcl.clause =
  let lits =
    List.map (fun atom -> - (Hashtbl.find az.var_of_atom atom)) conflicting
  in
  { Cdcl.lits = Array.of_list lits; learnt = true }

§ 05

The DPLL(T) loop

Identical to Part 2's cdcl except for one new case: when propagation finds no boolean conflict and every variable is assigned, ask the theory before declaring victory. A theory conflict is handled by the exact same handle_conflict as a boolean one - that reuse is the entire point of the architecture.

(* lib/dpll_t.ml, continued *)
 
let rec solve_loop (s : Cdcl.solver) (az : atomization) : bool option array option =
  match Cdcl.propagate s with
  | Some conflict ->
    (match Dpll_t.handle_conflict s conflict with
     | None -> None
     | Some () -> solve_loop s az)
  | None ->
    (match Cdcl.pick_branch s with
     | Some v ->
       s.Cdcl.dlevel <- s.Cdcl.dlevel + 1;
       Cdcl.enqueue s v None;
       solve_loop s az
     | None ->
       let atoms_now = true_atoms s az in
       (match Eq_theory.check az.num_terms atoms_now with
        | None -> Some (Array.copy s.Cdcl.value)   (* boolean-complete and theory-consistent *)
        | Some conflicting ->
          let clause = theory_clause az conflicting in
          s.Cdcl.clauses <- clause :: s.Cdcl.clauses;
          (match Dpll_t.handle_conflict s clause with
           | None -> None
           | Some () -> solve_loop s az)))

A subtlety worth naming: theory_clause always produces a clause that is currently falsified (every literal negates something that was just true), which is exactly what handle_conflict expects to analyze - a theory conflict and a boolean conflict are, from that function's point of view, indistinguishable.

(* handle_conflict does not know or care whether `conflict` came from
   Cdcl.propagate finding a falsified clause, or from a theory saying
   a set of atoms cannot hold - both are just `clause` values that are
   currently entirely false. *)

§ 06

A worked example: boolean-SAT but theory-UNSAT

Three atoms, three terms, and a boolean formula that forces all three atoms true with no boolean conflict whatsoever - the plain SAT layer alone would happily call this satisfiable.

let () =
  let atoms = [ Eq (0, 1); Eq (1, 2); Neq (0, 2) ] in
  let az = Atomize.make 3 atoms in
  let v_eq01 = Hashtbl.find az.var_of_atom (Eq (0, 1)) in
  let v_eq12 = Hashtbl.find az.var_of_atom (Eq (1, 2)) in
  let v_neq02 = Hashtbl.find az.var_of_atom (Neq (0, 2)) in
  let f = [ [ v_eq01 ]; [ v_eq12 ]; [ v_neq02 ] ] in
  let s = Cdcl.make_solver 3 f in
  match Dpll_t.solve_loop s az with
  | None -> print_endline "UNSAT"
  | Some _ -> print_endline "SAT"

What it prints - correctly UNSAT, even though every clause is a single positive unit literal and Part 2's plain CDCL over the same three clauses would return SAT immediately after one round of unit propagation.

UNSAT

Replacing the third clause with a disjunction gives the solver a real choice - now it is genuinely satisfiable, by picking the disequality's other option instead of forcing all three atoms true.

  let f = [ [ v_eq01 ]; [ v_eq12 ]; [ v_neq02; - v_eq01 ] ] in
  (* satisfied either by taking the disequality (theory-consistent only if
     0 and 2 are not forced equal - they still would be here via eq01/eq12,
     so the solver instead has to fall back on the other disjunct: -eq01) *)

Tracing what happens: the boolean layer first tries eq01=true, eq12=true (both forced units), which makes the third clause need v_neq02; asserting that triggers the same transitivity conflict as before, handle_conflict learns a clause, backjumps, and this time the solver is forced to flip eq01 to false instead - genuinely different boolean search driven entirely by a theory conflict.

SAT
(* model: eq01=false, eq12=true, neq02=true - consistent, since 0 and 2 are
   never forced into the same equivalence class *)

§ 07

What Part 4 plugs into this same interface

Nothing above the THEORY module signature and the check function inside it is specific to equality - solve_loop, handle_conflict, atomize, and theory_clause are all already generic. Part 4 swaps Eq_theory.check for a linear-arithmetic theory over the identical plumbing, with the same guarantee: any theory-level contradiction becomes a learned clause the boolean search can backjump on.

module type THEORY = sig
  val check : atom list -> atom list option
end
 
(* Part 4: Eq_theory.check is replaced by Diff_logic.check, deciding
   atoms of the shape `x - y <= k` via a negative-cycle check instead
   of union-find - solve_loop itself does not change at all. *)

← older

Profiling GHC Programs

2026-08-30

newer →

Introduction to Irmin

2026-09-05