This project is a Sudoku solver that uses a combination of computer vision and a SAT solver to solve Sudoku puzzles from an image, in under 500ms.

1. Preprocessing: The input image is processed using OpenCV to detect the Sudoku board and warp it into a top-down perspective.
2. Cell Detection: The individual cells of the Sudoku grid are detected and cut out to be used later on.
3. OCR: The digits in the cells are recognized using doctr's vitstr-small.
4. SAT-Solving: The Sudoku puzzle is converted into a satisfiability problem (SAT) and solved using the Kissat SAT solver.
5. Solution Rendering: The sat-compiled solution is rendered back onto the original image.

Prerequisites:

• Python 3 and pip
• Kissat SAT solver binary

1. Create & activate a virtual environment (optional but recommended):

conda create -n sat-sudoku -y python=3.13
conda activate sat-sudoku

2. Install Python dependencies:

pip install -r requirements.txt

3. Clone the repository:

git clone https://github.com/DD-65/sat-sudoku && cd sat-sudoku

4. Install Kissat and ensure it is on your PATH (or pass --kissat /path/to/kissat).

5. Verify the setup on the sample image:

python main.py sudoku.png

Notes:

• By default, torch runs on CPU. For improved performance, ensure it is configured to use CUDA, MPS, or another supported GPU backend.

python main.py path/to/sudoku.png

Flags:

• --kissat kissat Path to the kissat binary (default: kissat in PATH).
• --rows 9 Expected row count (default: 9).
• --cols 9 Expected column count (default: 9).
• --box 3x3 Subgrid size (use auto to infer for non-9x9).
• --timeout 10 Solver timeout in seconds.
• --out out Output directory for artifacts.
• --no-debug / -d Disable debug images, timings, and artifact files.
• --keep-solver-files Keep CNF/model temp files.

Artifacts (when debug is enabled) are written under --out:

• warped.png, sudoku.cnf, problem_summary.txt
• solver_stdout.txt, solver_stderr.txt
• solution_grid.json, solved_warped.png, solved_on_original.png

Use --compact-format to read multiple puzzles from a single file. Each puzzle is 81 characters (digits), with 0 or . as empty cells, and # to start a comment until end-of-line. This mode supports only standard 9x9 puzzles with 3x3 subgrids. (A commonly used sudoku database is the list of minimal sudokus (with only 17 hints) which can be downloaded from http://staffhome.ecm.uwa.edu.au/~00013890/sudokumin.php)

python main.py --compact-format path/to/db.txt

Outputs go to out/compact by default:

• DB_solved_1.png, DB_solved_2.png, ...
• Per-puzzle artifacts in out/compact/db_0001/, db_0002/, etc. (when debug is enabled)

cd generate_sudoku
python generator.py --difficulty 0.5

• --difficulty is a float in [0, 1] where higher is harder (default: 0.5).
• The generator saves the PNG to generate_sudoku/img/ when run from that folder.

Here's an example of the solver in action:

Input Image:

Output Image:

• The Sudoku generation feature uses the Algorithm outlined in this Stack Overflow post
• I got the idea for the --compact-format flag from another sudoku solver by bartp5