Solving Sudoku with AdaSAT

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 solvers, AdaSAT. In this blog post, I will use AdaSAT to implement a Sudoku solver.