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:

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:

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:

Now let’s look at our type-level boolean that we define as a GADT:

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:

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)$:

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:

Or with a = true, b = true, we use the second constructor:

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

would fail with a compile error:

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)$

Clause 2: $(b_0 \vee \neg b_1 \vee b_2)$

Clause 3: $(\neg b_1 \vee \neg b_2)$

Now we can introduce a formula GADT that defines the boolean variables and the conjunction of all the clauses in our CNF:

For example, we can construct a valid formula with the assignment b0=true, b1=true, b2=false:

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:

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:

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:

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:

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!