Implementing SAT in OCaml Part 4

2026-09-11 · 6 min

Full linear arithmetic needs a general Simplex tableau over arbitrary rational coefficients. Difference logic is the fragment where every atom has the shape x - y <= k - no general coefficients, just a bound on the gap between two variables. It is a real, standard SMT theory in its own right (scheduling and timing constraints are almost always expressed this way), and it reduces to a single, well-understood graph algorithm instead of a tableau: negative-cycle detection.

§ 01

Atoms as edges

x - y <= k is exactly the edge y -> x with weight k in a graph, using the standard shortest-paths encoding: if dist(x) <= dist(y) + k holds for every such edge, the system is consistent, and dist assigns a witness value to every variable.

(* lib/diff_logic.ml *)
 
type dl_atom = {
  x : int;      (* left variable *)
  y : int;      (* right variable *)
  k : float;    (* x - y <= k *)
}

A worked scheduling example before any code: three tasks with a fixed duration between two of them and a deadline, phrased as difference atoms. start_b - start_a <= -3 says task b cannot start until at least 3 time units after a; start_c - start_b <= -2 chains a third; start_a - start_c <= 4 caps the whole window at 4.

start_b - start_a <= -3     (* b starts >= 3 after a *)
start_c - start_b <= -2     (* c starts >= 2 after b *)
start_a - start_c <= 4      (* the whole chain fits in a window of 4 *)
summing all three: 0 <= -3 + -2 + 4 = -1, which is false -
no assignment of start times satisfies all three at once

§ 02

Bellman-Ford with a virtual zero source

Initializing every distance to 0 rather than infinity is the standard trick that makes this work without an explicit extra source vertex - it is equivalent to every variable having an implicit zero-weight edge from a shared virtual root, which does not change whether a negative cycle exists anywhere in the real graph.

let relax (dist : float array) (pred : int array) (pred_atom : dl_atom option array)
    (edges : dl_atom list) : bool =
  let changed = ref false in
  List.iter
    (fun e ->
      if dist.(e.y) +. e.k < dist.(e.x) then begin
        dist.(e.x) <- dist.(e.y) +. e.k;
        pred.(e.x) <- e.y;
        pred_atom.(e.x) <- Some e;
        changed := true
      end)
    edges;
  !changed

Relax |V| times: after |V|-1 rounds every shortest path (if the graph has no negative cycle) has stabilized, so a change on round |V| itself is the signature of a negative cycle.

let has_negative_cycle (nvars : int) (edges : dl_atom list) : bool =
  let dist = Array.make nvars 0.0 in
  let pred = Array.make nvars (-1) in
  let pred_atom = Array.make nvars None in
  let rec go i =
    if i > nvars then false
    else if relax dist pred pred_atom edges then go (i + 1)
    else false
  in
  ignore (go 1);
  relax dist pred pred_atom edges

That last call to relax is doing the actual detection - nvars rounds have already run inside go; one more round that still finds an improvement means a cycle is still shrinking, which only a negative cycle allows.

(* go runs relax up to nvars times or until it stabilizes early; either way,
   the final `relax dist pred pred_atom edges` on the last line is round
   nvars+1 - if it still finds an edge to relax, no finite shortest path
   exists, which is precisely a negative cycle *)

§ 03

Extracting the conflicting atoms

Detection alone is not enough - handle_conflict from Part 3 needs an actual list of atoms to turn into a clause. Rerun the same relaxation, keeping the predecessor pointers, find any edge that still relaxes, then walk pred backward nvars times to guarantee landing inside the cycle rather than on its approach path.

let find_negative_cycle (nvars : int) (edges : dl_atom list) : dl_atom list option =
  let dist = Array.make nvars 0.0 in
  let pred = Array.make nvars (-1) in
  let pred_atom : dl_atom option array = Array.make nvars None in
  for _ = 1 to nvars do
    ignore (relax dist pred pred_atom edges)
  done;
  let still_relaxes =
    List.find_opt (fun e -> dist.(e.y) +. e.k < dist.(e.x)) edges
  in
  match still_relaxes with
  | None -> None
  | Some e ->
    let start = ref e.x in
    for _ = 1 to nvars do start := pred.(!start) done;
    let cycle_start = !start in
    let rec collect v acc =
      match pred_atom.(v) with
      | None -> acc
      | Some a ->
        if v = cycle_start && acc <> [] then acc
        else collect pred.(v) (a :: acc)
    in
    Some (collect cycle_start [])

On the scheduling example from section 1, this returns exactly the three atoms that sum to a negative total - the smallest possible explanation, since dropping any one of them leaves a satisfiable pair.

# let atoms =
    [ { x = 1; y = 0; k = -3.0 };   (* start_b - start_a <= -3 *)
      { x = 2; y = 1; k = -2.0 };   (* start_c - start_b <= -2 *)
      { x = 0; y = 2; k =  4.0 } ]  (* start_a - start_c <= 4  *)
  in
  find_negative_cycle 3 atoms;;
- : dl_atom list option =
Some [{x=1; y=0; k=-3.}; {x=2; y=1; k=-2.}; {x=0; y=2; k=4.}]

§ 04

Plugging into the Part 3 interface

Wrapping the raw dl_atom-based functions into the atom/check shape Part 3's solve_loop already expects - the DL atom needs a boolean flag too, since a difference-logic literal can be negated (x - y > k is also expressible, just as a different bound on the same pair).

(* lib/dl_theory.ml *)
open Dpll_t
 
type dl_predicate = Le of int * int * float   (* x - y <= k *)
 
(* atoms as understood by Part 3's Atomize/Dpll_t machinery are just
   dl_predicate values here, instead of Part 3's Eq/Neq *)
 
let check (nvars : int) (true_atoms : dl_predicate list) : dl_predicate list option =
  let edges =
    List.map (function Le (x, y, k) -> ({ Diff_logic.x; y; k } : Diff_logic.dl_atom))
      true_atoms
  in
  match Diff_logic.find_negative_cycle nvars edges with
  | None -> None
  | Some cycle_edges ->
    Some
      (List.map
         (fun (e : Diff_logic.dl_atom) -> Le (e.x, e.y, e.k))
         cycle_edges)

This is the exact substitution Part 3's closing section promised - Eq_theory.check swapped for Dl_theory.check, with solve_loop, handle_conflict, and atomize completely unchanged. Only the atom type and its check function differ.

(* the same solve_loop from part 3, unmodified: *)
let solve_dl (nvars : int) (f : Cdcl.clause list) (atoms : dl_predicate list) =
  let az = Atomize.make nvars (List.map (fun a -> a) atoms) in
  let s = Cdcl.make_solver (List.length atoms) f in
  Dpll_t.solve_loop s az

§ 05

A boolean-satisfiable, theory-unsatisfiable scheduling instance

The three-task deadline problem from section 1, this time going through the full boolean-plus-theory solver rather than calling find_negative_cycle directly - each atom gets one clause forcing it true, exactly the shape that defeats a boolean-only solver but not this one.

let () =
  let atoms =
    [ Le (1, 0, -3.0); Le (2, 1, -2.0); Le (0, 2, 4.0) ]
  in
  let az = Atomize.make 3 atoms in
  let v1 = Hashtbl.find az.var_of_atom (List.nth atoms 0) in
  let v2 = Hashtbl.find az.var_of_atom (List.nth atoms 1) in
  let v3 = Hashtbl.find az.var_of_atom (List.nth atoms 2) in
  let f = [ [ v1 ]; [ v2 ]; [ v3 ] ] in
  let s = Cdcl.make_solver 3 f in
  match Dpll_t.solve_loop s az with
  | None -> print_endline "UNSAT: no feasible schedule"
  | Some _ -> print_endline "SAT"

What it prints.

UNSAT: no feasible schedule

Loosening the deadline to 6 instead of 4 makes it feasible - the same three atoms, but summing to +1 rather than -1, so no negative cycle exists and Bellman-Ford's dist array gives an actual witness schedule directly.

  let atoms = [ Le (1, 0, -3.0); Le (2, 1, -2.0); Le (0, 2, 6.0) ] in
  (* dist.(0)=0, dist.(1)=-3, dist.(2)=-5 is one valid witness:
     start_a=0, start_b=3, start_c=5, comfortably inside a window of 6 *)

§ 06

Reading a witness assignment off the graph

When check returns None (consistent), the dist array computed along the way already is a satisfying assignment - every variable's shortest distance from the virtual zero source is a value that respects every edge, by construction of Bellman-Ford itself. Exposing it means returning it instead of discarding it on success.

let check_with_model (nvars : int) (edges : Diff_logic.dl_atom list)
    : [ `Sat of float array | `Unsat of Diff_logic.dl_atom list ] =
  let dist = Array.make nvars 0.0 in
  let pred = Array.make nvars (-1) in
  let pred_atom : Diff_logic.dl_atom option array = Array.make nvars None in
  for _ = 1 to nvars do
    ignore (Diff_logic.relax dist pred pred_atom edges)
  done;
  match List.find_opt (fun e -> dist.(e.Diff_logic.y) +. e.Diff_logic.k < dist.(e.Diff_logic.x)) edges with
  | None -> `Sat dist
  | Some _ ->
    (match Diff_logic.find_negative_cycle nvars edges with
     | Some cycle -> `Unsat cycle
     | None -> assert false (* the relax check above already found one *))

On the feasible six-unit-window version, this hands back exact start times rather than just 'SAT'.

# check_with_model 3
    [ { x = 1; y = 0; k = -3.0 }; { x = 2; y = 1; k = -2.0 }; { x = 0; y = 2; k = 6.0 } ];;
- : [ `Sat of float array | `Unsat of Diff_logic.dl_atom list ] =
`Sat [|0.; -3.; -5.|]

§ 07

What general linear arithmetic adds beyond this

Named honestly rather than implemented: an atom with more than two variables and arbitrary rational coefficients - 3x + 2y - z <= 7 - has no graph representation at all, and needs a general Simplex tableau (the Dutertre-de Moura bounded-variable formulation used in most real DPLL(T) solvers) instead of Bellman-Ford. The check/conflict-explanation shape this post built stays the same either way; only what sits behind check changes.

difference logic:      x - y <= k            -> graph + Bellman-Ford (this post)
general linear arith:  sum(c_i * x_i) <= k    -> Simplex tableau, bounded variables
both plug into the same THEORY.check : atom list -> atom list option shape

← older

Introduction to Lean

2026-09-06

newer →

Introduction to Yojson

2026-09-12