In AdaCore’s Ada semantic analysis library, Libadalang, the type system is represented as a set of logical constraints or equations written in a domain-specific language (DSL) from our meta-compiler framework Langkit. These constraints model how types relate to each other (e.g., compatibility, conversions, subtypes, etc.). Rather than implementing a procedural or rule-based type checker, Libadalang translates these constraints into a logical form and solves them declaratively. This allows for greater flexibility, maintainability, and formal reasoning.

Originally, constraint solving in Libadalang was handled by several ad-hoc solvers built specifically for different parts of the type system. These implementations were tailored and somewhat fragile. A couple of years ago, a newer approach replaced these with a backend based on satisfiability (SAT) solvers, which offers several benefits:

• Robustness and performance: Modern SAT solvers are highly optimised and can efficiently handle large sets of constraints.
• Formalism: Expressing constraints as propositional logic formulas aligns better with verification tools and formal methods.
• Flexibility: The SAT-based infrastructure can evolve as the type system evolves, without rewriting the entire solver logic.

If you are curious about this work, the team published a paper at the 21st International Workshop on Satisfiability Modulo Theories: Application of SMT in a Meta-Compiler: A Logic DSL for Specifying Type Systems [Romain Béguet, Raphaël Amiard].

The SAT solver used by Libadalang is implemented in a standalone library cleverly called AdaSAT. In this blog post, I will use the methods described in this paper from Ines Lynce and Joel Ouaknine to implement a Sudoku solver with AdaSAT: Sudoku as a SAT Problem.

Sudoku as a SAT Problem

In SAT solving, a problem is expressed in conjunctive normal form (CNF), a conjunction (logical AND) of multiple clauses, which are disjunctions (logical OR) of one or more literals.

For example, the following formula is made up of 3 clauses:

(A ∨ B) ∧ (¬A ∨ C ∨ D) ∧ (¬B ∨ ¬C)

The SAT solver systematically evaluates combinations of truth values to establish whether the clauses can all be satisfied simultaneously, or if contradictions arise, determining the satisfiability of the overall problem.

How can we model the Sudoku puzzle this way?

We have to build a large formula for the SAT solver with various clauses constraining the puzzle.

To express the clauses, we will consider that each possible value for each cell is a variable (9 variables per cell). For instance, the variable V111 will tell whether or not the top leftmost cell contains the value 1, V568, whether or not the cell at row 5, column 6, contains the value 8, etc. With 9 columns, 9 rows, and 9 possible values per cell, we have 729 variables.

Once we run the formula through the solver, we will get a Boolean value for each of these variables. There should be exactly 81 True values, one for each cell.

For example, if the value at row 1, column 1 is 9, then by the rules of Sudoku the following conditions are met:

1. V119 is True

2. V1j9 is False for j /= 1 (no other 9's in column 1)

3. Vi19 is False for i /= 1 (no other 9's in row 1)

4. Vij9 is False when i in 2..3 and j in 2..3 (no other 9's in upper left grid of 9 squares)

How do we constrain the problem?

First, we will look at a single cell (e.g., 1, 1), we have 9 different variables: V111, V112, V113, …, V119.

We know that at least one of these variables must be true, because the cell contains at least one value.

V111 ∨ V112 ∨ V113 ∨ V114 ∨ … ∨ V119

This gives us one clause for the formula. Let’s see how to declare it.

In AdaSAT, variables are identified with positive numbers using the AdaSAT.Variable type, so we define a function to encode Vi,j,d (where i is the row, j the column, and d the value of the cell) into unique AdaSAT.Variable id value.

V111 will be variable id 1, V112 will be variable id 2, V568 will be variable id 377, V999 variable id 729.

AdaSAT provides objects to easily build clauses and formulas

For each cell, we add a clause to the formula as described above:

Next, we also know that only one of these variables can be true because each cell can hold only one value. There is an optimized way to specify “at most one of” in AdaSAT. It requires that the variable ids are contiguous, which is the case for the variable ids of the possible values of a single cell. For example, id 1 (V111) to 9 (V119) for the top-most left-most cell.

You get the idea. We then have to add clauses that specify that all cells per row and column have distinct values and that all cells per 3x3 square also have distinct values. I won’t copy the full code here; you can have a look at the GitHub repository for more details: github.com/Fabien-Chouteau/sudoku_sat.

How to specify the input grid?

But to solve a grid, we still have to specify the known values from the start of our Sudoku puzzle. To do that, we simply add a clause for each known value stating that the corresponding variable is true:

And finally, we can ask AdaSAT to solve our puzzle, like so:

Model is an array of Variable_Value which can either be True, False, or Unset. Each element of the array corresponds to one of the 729 variables used in our formula. We initialize all values to Unset.

And finally, we call DPPL_Solve (DPLL being the name of the algorithm wikipedia.org/wiki/DPLL_algorithm). The function returns true if the formula is satisfiable, which should always be the case here because the Sudoku puzzle is always satisfiable (given a valid input grid), and the DPLL algorithm is said to be “complete”. Afterward, the Model array contains either True or False for each of the variables.

We can extract the value for each cell by looking at the variables set to True.

And so this is how we print the result grid:

As you can see, AdaSAT is really easy to use and can easily be integrated into your own project, if you need to schedule sports events, for instance.

If you are new to SAT and want to know more, I recommend this video by Dr. Alexander Kulikov: https://www.youtube.com/watch?v=4K1MyG4ljI8