One of my recent interests has been in solving problems with various kinds of satisfiability solvers. As an introduction to this idea I want to demonstrate how to create a sudoku solver with almost no effort by reduction to a common satisfiability problem (CNF-SAT) and using an existing solver (MiniSat).
Solving sudoku by reduction to CNF-sat is hardly a new idea, I’m sure a quick google would show various approaches. If the mathematical notation below looks a little scary perhaps try reading the code further down, it really is quite simple if you can read propositional formulas.
A quick sudoku recap
A sudoku puzzle is a 9×9 grid of cells, split into 9 non overlapping 3×3 “boxes”. Some of these will be labelled with a digit from 1 to 9, others will be blank. The aim is to label the remaining cells so that every row, column and box contains the digits 1 through 9.
Perhaps the most well known satisfiability problem is propositional satisfiability: given a formula in propositional logic can we find assignments for all the variables which makes the formula true? A subset of this problem is satisfiability on formulas in conjunctive normal form (CNF-SAT). A formula is in conjunctive normal form if it is a conjunction of clauses, where a clause is a disjunction of literals (a literal is just a variable or its negation), e.g
\[ (a \vee \neg b) \wedge (\neg a \vee c \vee d) \wedge (\neg b \vee \wedge \neg d) \] \[ a \wedge (\neg a \wedge \neg b) \]