SAT Sudoku solver

A SAT-based Sudoku solver made in the context of a small project in the "Logic Problem Solving" class in the first year at the Polytech Paris-Saclay engineering school

Requirements

pip install -r requirements.txt

• Solver made using pycosat and a bit of numpy
• GUI made using tkinter

Run tests

Download the 1 million Sudoku games dataset by @Kyubyong (sudoku.csv)

Run solver.py to run the tests

GUI

Run main.py to enter any sudoku puzzle and solve it

Credits

Co-developed by:

• Alexandre Malfreyt
• Esteban Bruneau

TODO

• Coding every constraint from sudoku rules into a CNF formula
  • Solving sudoku using pycosat
• Testing using a sudoku dataset
  • Timing the solve() function
• GUI using tkinter
  • Make sure we can only enter numbers 1-9 in the GUI
  • Show a popup if the sudoku grid has no solution
  • Separate every 3x3 sub-grid
• Generate sudoku grids
  • Generate sudoku grids using a CNF
• Count the number of solutions
• Working with n^2 * n^2 sudoku grids