We encode Sudokus and Hyper Sudokus as SAT problems, solve them, and obtain some relevant (to us :)) statistics.
We use three types of encodings: minimal encoding, extended encoding, and efficient encoding.
The SAT solvers involved are PicoSAT (via pycosat bindings), zChaff, and WalkSAT.
You need to install WalkSAT and zChaff first.
Packages required:
pip install argparse
pip install pycosat
Solve 10 standard Sudokus from a the provided data set (where best indicates the WalkSAT variant to use; the other variants are novelty, and rnovelty)
python solver.py data/sudoku_1000.csv 10 best
Solve 10 Hyper Sudokus from a the provided data set, using novelty as a WalkSAT variant
python hyper.py data/hyper.txt 30 novelty