Implementing SAT in OCaml Part 1

2026-08-21 · 7 min

§ 01

Project layout

One library, one executable. Every later part in this series adds to sat_lib rather than replacing it.

satproj/
├── lib/
│   ├── dune
│   └── sat.ml
├── bin/
│   ├── dune
│   └── main.ml
└── dune-project

dune-project.

(lang dune 3.16)

lib/dune.

(library
 (name sat_lib))

bin/dune.

(executable
 (name main)
 (libraries sat_lib))

§ 02

CNF: the representation

A literal is a nonzero int - positive means the variable, negative means its negation. A clause is a disjunction of literals; a formula is a conjunction of clauses. This is the whole data model.

(* lib/sat.ml *)
 
type lit = int
type clause = lit list
type formula = clause list
 
let var (l : lit) : int = abs l
let neg (l : lit) : lit = -l

A partial assignment maps a variable to a bool. Hashtbl rather than an array, since we do not fix the variable count up front in this first version.

type assignment = (int, bool) Hashtbl.t
 
let make_assignment () : assignment = Hashtbl.create 64

value looks up a literal's truth under an assignment, applying the sign - None if its variable is unassigned.

let value (a : assignment) (l : lit) : bool option =
  match Hashtbl.find_opt a (var l) with
  | None -> None
  | Some b -> Some (if l > 0 then b else not b)
 
let assign (a : assignment) (l : lit) : unit =
  Hashtbl.replace a (var l) (l > 0)
 
let unassign (a : assignment) (v : int) : unit =
  Hashtbl.remove a v

A tiny formula to test everything against as it is built: (x1 or x2), (not x1 or x3), (not x2 or not x3). Satisfiable - for example x1=true, x2=false, x3=true.

let example : formula =
  [ [ 1; 2 ]; [ -1; 3 ]; [ -2; -3 ] ]

§ 03

Satisfaction and conflict

A clause is satisfied if some literal in it is true. A clause is falsified if every literal in it is assigned and false - an empty clause is vacuously falsified, which is exactly the right behavior: an empty clause means unsatisfiable.

let clause_satisfied (a : assignment) (c : clause) : bool =
  List.exists (fun l -> value a l = Some true) c
 
let clause_falsified (a : assignment) (c : clause) : bool =
  List.for_all (fun l -> value a l = Some false) c
 
let formula_satisfied (a : assignment) (f : formula) : bool =
  List.for_all (clause_satisfied a) f
 
let has_conflict (a : assignment) (f : formula) : bool =
  List.exists (clause_falsified a) f

§ 04

Unit propagation

A clause is unit if it is not yet satisfied and has exactly one unassigned literal - that literal must be true, or the clause cannot be satisfied at all.

let unit_literal (a : assignment) (c : clause) : lit option =
  if clause_satisfied a c then None
  else
    match List.filter (fun l -> value a l = None) c with
    | [ l ] -> Some l
    | _ -> None
 
let find_unit (a : assignment) (f : formula) : lit option =
  List.find_map (unit_literal a) f

Propagate to a fixpoint: assign every forced literal, which can create new unit clauses, until none remain.

let rec unit_propagate (a : assignment) (f : formula) : unit =
  match find_unit a f with
  | Some l -> assign a l; unit_propagate a f
  | None -> ()

Tracing it by hand on the example formula, after deciding x1 = true. (x1 or x2) is already satisfied; (not x1 or x3) becomes unit on x3, forcing x3 = true; that makes (not x2 or not x3) unit on not x2, forcing x2 = false.

assign x1 = true
unit_propagate:
  (-1 3) is unit on 3    -> assign x3 = true
  (-2 -3) is unit on -2  -> assign x2 = false
  no more unit clauses
result: x1=true, x2=false, x3=true  (matches the formula's only two models)

§ 05

Picking a variable, and the core DPLL loop

Every variable mentioned anywhere in the formula, deduplicated - used to find something left to branch on.

let all_vars (f : formula) : int list =
  List.sort_uniq compare (List.concat_map (List.map var) f)
 
let unassigned_var (a : assignment) (f : formula) : int option =
  List.find_opt (fun v -> Hashtbl.find_opt a v = None) (all_vars f)

The recursive search. Propagate first; if that produces a conflict, this branch is dead. If everything is satisfied, done. Otherwise pick an unassigned variable and try both values, undoing between attempts by restoring a saved copy of the assignment - correctness over speed, for a first version.

let rec dpll (a : assignment) (f : formula) : bool =
  unit_propagate a f;
  if has_conflict a f then false
  else if formula_satisfied a f then true
  else
    match unassigned_var a f with
    | None -> true   (* every variable assigned, nothing falsified: satisfied *)
    | Some v ->
      let saved = Hashtbl.copy a in
      Hashtbl.replace a v true;
      if dpll a f then true
      else begin
        Hashtbl.reset a;
        Hashtbl.iter (Hashtbl.replace a) saved;
        Hashtbl.replace a v false;
        dpll a f
      end

The public entry point.

let solve (f : formula) : assignment option =
  let a = make_assignment () in
  if dpll a f then Some a else None

Trying it on the example, and on a trivially unsatisfiable formula: x1 and not x1, as two unit clauses that immediately conflict.

# solve example;;
- : assignment option = Some <abstr>   (* x1=true, x2=false, x3=true *)
 
# solve [ [ 1 ]; [ -1 ] ];;
- : assignment option = None

§ 06

Pure literal elimination

A literal is pure if its variable appears with only one polarity across every clause that still matters. A pure literal can always be set to make it true without ever causing a conflict, since no clause needs the opposite polarity - this is a second, cheap simplification alongsideunit propagation.

Scan every unassigned occurrence and track whether each variable has been seen positive, negative, or both.

let pure_literals (a : assignment) (f : formula) : lit list =
  let polarity : (int, bool option) Hashtbl.t = Hashtbl.create 64 in
  List.iter
    (fun c ->
      if not (clause_satisfied a c) then
        List.iter
          (fun l ->
            if value a l = None then begin
              let v = var l in
              let sign = l > 0 in
              match Hashtbl.find_opt polarity v with
              | None -> Hashtbl.replace polarity v (Some sign)
              | Some (Some s) when s <> sign -> Hashtbl.replace polarity v None
              | _ -> ()
            end)
          c)
    f;
  Hashtbl.fold
    (fun v pol acc -> match pol with
      | Some sign -> (if sign then v else -v) :: acc
      | None -> acc)
    polarity []

Folded into a combined simplification step, run to a fixpoint alongside unit propagation - each pass can unlock new pure literals, and vice versa.

let rec simplify (a : assignment) (f : formula) : unit =
  unit_propagate a f;
  match pure_literals a f with
  | [] -> ()
  | ls -> List.iter (assign a) ls; simplify a f

dpll now calls simplify instead of unit_propagate directly - everything else is unchanged, since pure literal assignment can never itself introduce a conflict.

let rec dpll (a : assignment) (f : formula) : bool =
  simplify a f;
  if has_conflict a f then false
  else if formula_satisfied a f then true
  else
    match unassigned_var a f with
    | None -> true
    | Some v ->
      let saved = Hashtbl.copy a in
      Hashtbl.replace a v true;
      if dpll a f then true
      else begin
        Hashtbl.reset a;
        Hashtbl.iter (Hashtbl.replace a) saved;
        Hashtbl.replace a v false;
        dpll a f
      end

§ 07

Why this blows up: pigeonhole

The classic hard case for plain DPLL with no learning: n+1 pigeons into n holes, unsatisfiable, but every branch looks identical to the search until it is fully explored - exponentially many dead ends with no way to remember why. Variables p(i,j) mean pigeon i is in hole j.

let pigeonhole (pigeons : int) (holes : int) : formula =
  let var_id i j = 1 + (i * holes) + j in
  let at_least_one_hole =
    List.init pigeons (fun i -> List.init holes (fun j -> var_id i j))
  in
  let no_shared_hole =
    List.concat
      (List.init holes (fun j ->
        List.concat
          (List.init pigeons (fun i1 ->
            List.filter_map
              (fun i2 ->
                if i2 > i1 then Some [ -(var_id i1 j); -(var_id i2 j) ] else None)
              (List.init pigeons (fun k -> k))))))
  in
  at_least_one_hole @ no_shared_hole

Four pigeons into three holes solves fast enough to try; six into five already takes noticeably longer on this solver, with no learning to remember that a whole class of branches is doomed for the same underlying reason. This is exactly the gap Part 2 closes.

# solve (pigeonhole 4 3);;
- : assignment option = None

§ 08

Reading DIMACS CNF

DIMACS CNF is the standard input format for SAT solvers and benchmark sets: a header line stating the variable and clause counts, then one line per clause, each ending in a literal 0. Reading it is what lets this solver run against real benchmarks in Part 5.

A small example file - the pigeonhole-4-into-3 instance is exactly this shape, generated instead of hand-written.

c four pigeons, three holes
p cnf 12 18
1 2 3 0
4 5 6 0
-1 -4 0
...

The parser: skip comment lines starting with c, read the problem line for bookkeeping only, then read clauses until the trailing 0 of each - split on whitespace since DIMACS clauses may span line breaks in principle, though real files rarely do.

let parse_dimacs (path : string) : formula =
  let ic = open_in path in
  let buf = Buffer.create 4096 in
  (try
     while true do
       let line = input_line ic in
       if String.length line = 0 || line.[0] = 'c' || line.[0] = 'p' then ()
       else begin Buffer.add_string buf line; Buffer.add_char buf ' ' end
     done
   with End_of_file -> ());
  close_in ic;
  let tokens =
    String.split_on_char ' ' (Buffer.contents buf)
    |> List.filter (fun s -> s <> "")
    |> List.map int_of_string
  in
  let rec group acc current = function
    | [] -> List.rev acc
    | 0 :: rest -> group (List.rev current :: acc) [] rest
    | l :: rest -> group acc (l :: current) rest
  in
  group [] [] tokens

Writing a formula back out, for generating benchmark files from pigeonhole/other generators rather than hand-typing them.

let write_dimacs (path : string) (f : formula) : unit =
  let oc = open_out path in
  let nvars = List.fold_left (fun m c -> List.fold_left (fun m l -> max m (var l)) m c) 0 f in
  Printf.fprintf oc "p cnf %d %d\n" nvars (List.length f);
  List.iter
    (fun c ->
      List.iter (fun l -> Printf.fprintf oc "%d " l) c;
      Printf.fprintf oc "0\n")
    f;
  close_out oc

§ 09

A command-line driver

Printing a satisfying model in DIMACS's own convention: one line, positive or negative literal per variable, terminated by 0.

(* lib/sat.ml, continued *)
 
let print_model (f : formula) (a : assignment) : unit =
  List.iter
    (fun v ->
      let l = if Hashtbl.find a v then v else -v in
      Printf.printf "%d " l)
    (all_vars f);
  print_endline "0"

bin/main.ml - reads a DIMACS file from argv, solves it, reports SAT/UNSAT, and prints the model on success.

let () =
  if Array.length Sys.argv <> 2 then begin
    prerr_endline "usage: main <file.cnf>";
    exit 2
  end;
  let f = Sat_lib.parse_dimacs Sys.argv.(1) in
  match Sat_lib.solve f with
  | None -> print_endline "UNSAT"
  | Some a ->
    print_endline "SAT";
    Sat_lib.print_model f a

Build and run against a generated pigeonhole instance.

$ dune build
$ dune exec ./bin/main.exe -- pigeon.cnf

What it prints for a satisfiable instance - three pigeons, four holes, so one hole is always left empty and every assignment of pigeons to distinct holes is a model.

SAT
1 -2 -3 -4 5 -6 -7 -8 -9 10 -11 -12 0

← older

Functional Programming in C++

2026-08-16

newer →

Introduction to odoc

2026-08-23