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