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:

  1. Transform the SAT problem into conjunctive normal form (CNF) via the Tseitin transformation in polynomial time
  2. Transform each CNF clause into a Generalized Algebraic Data Type (GADT) “proof type” where constructors represent ways to satisfy the clause
  3. 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 type true_ bool - it cannot create false_ bool
  • F has type false_ bool - it cannot create true_ 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:

  1. When the first variable is false and the second variable is anything, we can construct a value with (C1_by_not_a)
  2. 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 vs number of variables

Compilation time exhibits exponential growth

Memory usage vs number of variables

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!