Sudoku Solver (OCaml + Z3)

Encodes 9x9 or 16x16 Sudoku to CNF, solves with Z3, and decodes back to a completed grid.

Requirements

• OCaml compiler (ocamlc)
• Z3 SAT solve

How to Run

Option 1: Using Makefile (Single Solution)

make clean
make
make run

Pipeline:

1. ./sudoku2cnf input.txt > problem.cnf - Encode puzzle to CNF
2. z3 -dimacs problem.cnf > sat_output.txt - Solve with Z3
3. ./sol2grid sat_output.txt > output.txt - Decode solution

Expected Output: output.txt contains the solved Sudoku grid (if exists) or No solution exists.

Option 2: Using Makefile.multi (Uniqueness Check)

make -f Makefile.multi clean
make -f Makefile.multi
make -f Makefile.multi run

Pipeline:

1. ./sudoku2cnf input.txt > problem.cnf - Encode puzzle to CNF
2. z3 -dimacs problem.cnf > sat_output.txt - Solve with Z3
3. ./sol2grid2 sat_output.txt > output.txt - Decode and check uniqueness

Expected Output: output.txt contains the solved grid + uniqueness message (Unique solution or Multiple solutions) or No solution.

Input Format

• One row per line, use . for empty cells
• 9x9: digits 1-9
• 16x16: digits 0-9 and letters A-F

Example input.txt (9x9):

53..7....
6..195...
.98....6.
8...6...3
4..8.3..1
7...2...6
.6....28.
...419..5
....8..79

Validation (Optional)

make check

Verifies the solution against the original puzzle.

Procedure

About sudoku2cnf.ml

• Reads Sudoku from input.txt
• Writes clauses in DIMACS format to problem.cnf
• 5 types of constraints are written -> givens -> at least one value per cell -> at most one value per cell -> row uniqueness -> column uniqueness -> block uniqueness
• map function used for variable indexing, e.g., for 9x9: var(i,j,v) = 81*(v-1) + 9*i + j + 1
• all the print statements for clauses are written along with the constraints
• clauses are counted before hand to write the header, = given_numbers_in_sudoku + (size * size) + (size * size * choose2 size) + 3 * (size * size * choose2 size)

About sol2grid.ml

• Reads Z3 output from sat_output.txt
• if first line is s UNSATISFIABLE, prints No solution exists
• else reads variable assignments, filters positive ones and decodes them back to grid format
• uses inverse of map function to decode variable indices back to (i,j,v)

About sol2grid2.ml

• Similar to sol2grid.ml but also checks for uniqueness
• After decoding the first solution, adds a clause to block that solution and re-runs Z3
• If second solution found, prints Multiple solutions, else Unique solution