This is the implementation of the SAT sudoku solver based on the paper by Inês Lynce and Jöel Ouaknine titled Sudoku as a SAT Problem.

Sudoku is modeled as the SAT problem. The idea is to formulate a sudoku puzzle as a SAT formula if the puzzle has a solution. Then we use the SAT program to find the solution.

SAT is a program that solves the satisfiability problem: given a formula, it either returns an assignment that makes it true, or says that no such assignment exists. It uses a restricted form of propositional formula called CNF (Conjunctive Normal Form). CNF consists of a set of clauses, each of which is a set of literals. A literal is a variable or its negation. Each clause is interpreted as the disjunction of its literals, and the formula as a whole is interpreted as the conjunction of the clauses.

This project uses MiniSat's Rust reimplementation RatSat.

For the in-depth explanation of how the sudoku solver works, see the paper.

$ ./solve A_PATH_TO_THE_PUZZLE

There are 9 sample sudoku puzzles available under directory named puzzles. To solve the first puzzle, simply run ./solve puzzles/sudoku1.puzzle.

• Inês Lynce and Jöel Ouaknine, Sudoku as a SAT Problem
• RatSat
• MiniSat
• Sudoku

MIT License