Encoding SAT in OCaml GADTs
In this post, I’ll show how to encode boolean satisfiability (SAT) problems with OCaml’s GADTs, tricking the compiler into becoming a SAT solver and proving that compiling OCaml is NP-hard.
Previous Work
It’s worth mentioning that abusing OCaml types for compile-time computation is an established tradition. Here are a few examples that directly inspired and informed this post:
- OCamlPro’s EZSudoku encoded Sudoku puzzles in GADTs using refutation cases to find solutions (implying compiling OCaml is NP-hard)
- Garrigue & Le Normand (2015) proved that exhaustiveness checking for GADTs is undecidable by encoding the halting problem
The Overall Strategy
Encoding the SAT problem in OCaml types works in three steps:
- Transform the SAT problem into conjunctive normal form (CNF) via the Tseitin transformation in polynomial time
- Transform each CNF clause into a Generalized Algebraic Data Type (GADT) “proof type” where constructors represent ways to satisfy the clause
- Combine all clause proofs into a single “formula” type that can only be constructed when all clauses are simultaneously satisfiable
When we try to refute all possible formula constructions, the compiler either succeeds (formula is unsatisfiable) or fails with a counterexample that reveals the satisfying assignment.
Type-Level Booleans
Before getting into type-level booleans and our GADTs, let’s first review regular algebraic data types (ADTs) with an example. Typically you might define a boolean type with an ADT as:
type regular_bool =
| T
| F
With this regular type, both T
and F
constructors create values of the same
type regular_bool
. Both let x = T
and let y = F
have type regular_bool
,
so both let (x : regular_bool) = T
and let (y : regular_bool) = F
will
compile.
If you write a function that takes a regular_bool
, you have to match on both
cases, otherwise the compiler will complain. For example:
let foo (b : regular_bool) =
match b with
| T -> "Uh huh"
| F -> "Nuh uh"
Now let’s look at our type-level boolean that we define as a GADT:
type true_ = private Tag_true
type false_ = private Tag_false
type 'a bool =
| T : true_ bool
| F : false_ bool
With GADTs, constructors can return constrained types. In our definition:
-
T
has typetrue_ bool
- it cannot createfalse_ bool
-
F
has typefalse_ bool
- it cannot createtrue_ bool
This constraint is enforced at compile time. For example, let (x : false_ bool)
= T
will give a compile error, since T
has type true_ bool
, not false_
bool
.
The compiler uses these constraints during exhaustiveness checking when pattern
matching. That means that if you have a function that takes true_ bool
, the
compiler can determine that only the T
constructor is possible:
let only_true (b : true_ bool) =
match b with
| T -> "Yep, it's true"
| F -> . (* This syntax declares a "refutation case". Either the compiler
agrees this case is impossible to occur, or it fails to
compile with an error. Alternatively, we could have left this
case off altogether and just matched T, implicitly refuting F. *)
You might be thinking: “Wow, that seems hard for the compiler to do in general”. And you’d be right! This exhaustiveness checking is what will ultimately power the SAT solving.
Clauses as Proof Types
Great, now that we have type-level booleans, we can move on with encoding CNF clauses. In our encoding, each CNF clause becomes a GADT where constructors represent different satisfying conditions. Consider the clause $(\neg a \vee b)$:
type ('a, 'b) clause1_proof =
| C1_by_not_a : (false_, 'b) clause1_proof
| C1_by_b : ('a, true_) clause1_proof
This proof type can be constructed in two ways:
- When the first variable is false and the second variable is anything, we can
construct a value with (
C1_by_not_a
) - When the second variable is true and the first variable is anything, then we
use (
C1_by_b
).
For example, with variables a = false, b = true
, we can construct:
let (proof : (false_, true_) clause1_proof) = C1_by_not_a
Or with a = true, b = true
, we use the second constructor:
let (proof : (true_, true_) clause1_proof) = C1_by_b
If the a
and b
bools don’t satisfy the original clause, you’ll find that
there is no constructor we could choose, so it would be impossible to construct
a value of the proof type. For example, trying something like
let (proof : (true_, false_) clause1_proof) = C1_by_b
would fail with a compile error:
Error: The constructor "C1_by_b" has type "(true_, true_) clause1_proof"
but an expression was expected of type "(true_, false_) clause1_proof"
Type "true_" is not compatible with type "false_"
Conjunction
Let’s assume we want to encode the CNF formula: $(\neg b_0 \vee b_1) \wedge (b_0 \vee \neg b_1 \vee b_2) \wedge (\neg b_1 \vee \neg b_2)$
We’d have three clause proof types as described above:
Clause 1: $(\neg b_0 \vee b_1)$
type ('b0, 'b1) clause1_proof =
| C1_by_not_b0 : (false_, 'b1) clause1_proof
| C1_by_b1 : ('b0, true_) clause1_proof
Clause 2: $(b_0 \vee \neg b_1 \vee b_2)$
type ('b0, 'b1, 'b2) clause2_proof =
| C2_by_b0 : (true_, 'b1, 'b2) clause2_proof
| C2_by_not_b1 : ('b0, false_, 'b2) clause2_proof
| C2_by_b2 : ('b0, 'b1, true_) clause2_proof
Clause 3: $(\neg b_1 \vee \neg b_2)$
type ('b1, 'b2) clause3_proof =
| C3_by_not_b1 : (false_, 'b2) clause3_proof
| C3_by_not_b2 : ('b1, false_) clause3_proof
Now we can introduce a formula
GADT that defines the boolean variables and the
conjunction of all the clauses in our CNF:
type formula =
Formula :
(* Introduce the variables *)
'b0 bool *
'b1 bool *
'b2 bool *
(* All clause proofs must exist for these variables *)
('b0, 'b1) clause1_proof *
('b0, 'b1, 'b2) clause2_proof *
('b1, 'b2) clause3_proof ->
formula
For example, we can construct a valid formula with the assignment b0=true, b1=true, b2=false
:
let solution = Formula (T, T, F, C1_by_b1, C2_by_b0, C3_by_not_b2)
But we cannot construct a formula like Formula (T, T, T, _, _, _)
because no
combination of proof constructors exists that satisfies all clauses with
b0=true, b1=true, b2=true
.
Refutation and Exhaustiveness Checking
The following match and refutation triggers the type checker’s exhaustiveness checking:
let solve (formula : formula) =
match formula with
| Formula _ -> .
This syntax claims to the compiler that “no formula values can exist”. If the formula is actually satisfiable, the compiler disagrees and provides a counterexample:
Error: This match case could not be refuted.
Here is an example of a value:
Formula (T, T, F, C1_by_b1, C2_by_b0, C3_by_not_b2)
The error message contains a solution: $b_0 = \text{true}, b_1 = \text{true}, b_2 = \text{false}$.
If the formula is unsatisfiable, then the OCaml program will compile since the compiler agrees with the refutation. There we have it!
Script
A Python script automates the
conversion of a pysat
boolean expression to an OCaml file. You’re welcome to
use it for your OCaml SAT solving needs! For example, it can be used as simply
as:
from pysat.formula import *
alice, bob, charlie = Atom("alice"), Atom("bob"), Atom("charlie")
formula = And(Or(~alice, bob), Or(alice, ~bob, charlie), Or(~bob, ~charlie))
print(to_ocaml(formula))
Results
The OCaml compiler can in fact solve small SAT problems! For example, the $N$-Queens Problem on very small $N$:
N-Queens | Variables | Clauses | Time | Memory | Result |
---|---|---|---|---|---|
N=1 | 1 | 1 | ~0.01s | 16 MB | ✅ SAT |
N=2 | 4 | 8 | ~0.01s | 17 MB | ❌ UNSAT |
N=3 | 9 | 31 | 0.21s | 55 MB | ❌ UNSAT |
N=4 | 16 | 80 | 8h+ | 800 GB+ | ⏳️ Timeout |
Including benchmarks on the Pigeonhole Principle, time and memory usage unsurprisingly scale exponentially:
Compilation time exhibits exponential growth
Memory consumption follows similar exponential scaling
Conclusion
It’s common in OCaml and other strongly typed functional languages to encode invariants in types for safer programming. I hope this post helps you unlock even stronger type-level guarantees in your projects. :) Thanks for reading!