_____ __ __ _____ _____ _____ __
/ ___/__ ______/ /___ / /____ __ /__ / |__ / / ___/____ / / _____ _____
\__ \/ / / / __ / __ \/ //_/ / / / / / /_ < \__ \/ __ \/ / | / / _ \/ ___/
___/ / /_/ / /_/ / /_/ / ,< / /_/ / / /_____/ / ___/ / /_/ / /| |/ / __/ /
/____/\__,_/\__,_/\____/_/|_|\__,_/ /____/____/ /____/\____/_/ |___/\___/_/
Sudoku Z3 Solver
A Sudoku solver that accepts a jpeg image of a standard 9x9 Sudoku grid, attempts to extract the problem from it and solve it using the Z3 solver.
Usage example with the provided sample image
$> python sudoku-Z3-solver.py -img sample_image.jpg
[+] Extracting sudoku puzzle from: sample_image.jpg
[+] Problem Puzzle:
+–––––––––+–––––––––+–––––––––+
| 0 0 0 | 0 0 0 | 2 0 0 |
| 0 0 0 | 0 2 0 | 0 3 0 |
| 2 0 5 | 1 9 0 | 0 0 6 |
+–––––––––+–––––––––+–––––––––+
| 0 0 0 | 0 1 4 | 0 6 3 |
| 0 3 0 | 0 0 0 | 0 7 0 |
| 4 2 0 | 9 3 0 | 0 0 0 |
+–––––––––+–––––––––+–––––––––+
| 1 0 0 | 0 6 2 | 5 0 9 |
| 0 6 0 | 0 5 0 | 0 0 0 |
| 0 0 4 | 0 0 0 | 0 0 0 |
+–––––––––+–––––––––+–––––––––+
[+] Sovling using Z3
Solved: True
PROBLEM SOLUTION
+–––––––––+–––––––––+–––––––––+ +–––––––––+–––––––––+–––––––––+
| 0 0 0 | 0 0 0 | 2 0 0 | | 3 1 7 | 6 4 8 | 2 9 5 |
| 0 0 0 | 0 2 0 | 0 3 0 | | 6 8 9 | 7 2 5 | 1 3 4 |
| 2 0 5 | 1 9 0 | 0 0 6 | | 2 4 5 | 1 9 3 | 7 8 6 |
+–––––––––+–––––––––+–––––––––+ +–––––––––+–––––––––+–––––––––+
| 0 0 0 | 0 1 4 | 0 6 3 | | 7 5 8 | 2 1 4 | 9 6 3 |
| 0 3 0 | 0 0 0 | 0 7 0 | | 9 3 1 | 5 8 6 | 4 7 2 |
| 4 2 0 | 9 3 0 | 0 0 0 | | 4 2 6 | 9 3 7 | 8 5 1 |
+–––––––––+–––––––––+–––––––––+ +–––––––––+–––––––––+–––––––––+
| 1 0 0 | 0 6 2 | 5 0 9 | | 1 7 3 | 8 6 2 | 5 4 9 |
| 0 6 0 | 0 5 0 | 0 0 0 | | 8 6 2 | 4 5 9 | 3 1 7 |
| 0 0 4 | 0 0 0 | 0 0 0 | | 5 9 4 | 3 7 1 | 6 2 8 |
+–––––––––+–––––––––+–––––––––+ +–––––––––+–––––––––+–––––––––+
Usage example without any arguments
This uses the problem grid defined within the source code as the default problem
$> python sudoku-Z3-solver.py
[+] Problem Puzzle:
+–––––––––+–––––––––+–––––––––+
| 8 0 0 | 0 0 0 | 0 0 0 |
| 0 0 3 | 6 0 0 | 0 0 0 |
| 0 7 0 | 0 9 0 | 2 0 0 |
+–––––––––+–––––––––+–––––––––+
| 0 5 0 | 0 0 7 | 0 0 0 |
| 0 0 0 | 0 4 5 | 7 0 0 |
| 0 0 0 | 1 0 0 | 0 3 0 |
+–––––––––+–––––––––+–––––––––+
| 0 0 1 | 0 0 0 | 0 6 8 |
| 0 0 8 | 5 0 0 | 0 1 0 |
| 0 9 0 | 0 0 0 | 4 0 0 |
+–––––––––+–––––––––+–––––––––+
[+] Sovling using Z3
Solved: True
PROBLEM SOLUTION
+–––––––––+–––––––––+–––––––––+ +–––––––––+–––––––––+–––––––––+
| 8 0 0 | 0 0 0 | 0 0 0 | | 8 1 2 | 7 5 3 | 6 4 9 |
| 0 0 3 | 6 0 0 | 0 0 0 | | 9 4 3 | 6 8 2 | 1 7 5 |
| 0 7 0 | 0 9 0 | 2 0 0 | | 6 7 5 | 4 9 1 | 2 8 3 |
+–––––––––+–––––––––+–––––––––+ +–––––––––+–––––––––+–––––––––+
| 0 5 0 | 0 0 7 | 0 0 0 | | 1 5 4 | 2 3 7 | 8 9 6 |
| 0 0 0 | 0 4 5 | 7 0 0 | | 3 6 9 | 8 4 5 | 7 2 1 |
| 0 0 0 | 1 0 0 | 0 3 0 | | 2 8 7 | 1 6 9 | 5 3 4 |
+–––––––––+–––––––––+–––––––––+ +–––––––––+–––––––––+–––––––––+
| 0 0 1 | 0 0 0 | 0 6 8 | | 5 2 1 | 9 7 4 | 3 6 8 |
| 0 0 8 | 5 0 0 | 0 1 0 | | 4 3 8 | 5 2 6 | 9 1 7 |
| 0 9 0 | 0 0 0 | 4 0 0 | | 7 9 6 | 3 1 8 | 4 5 2 |
+–––––––––+–––––––––+–––––––––+ +–––––––––+–––––––––+–––––––––+
TO DO
- Accept sudoku image (jpg) from commandline, extract problem and solve using Z3.
- Accept problem string from command line
- Expose the sum contraints functionality, provision to accept the constraints from the command line