This is a Sudoku solver based on PicoSAT, using the python wrapper pycosat. See more about SAT here.

Four constraints are applied:

• Each cell is filled with one and only one digit from 1 to 9.
• Each row contains all nine different digits.
• Each column contains all nine different digits.
• Each sub-box contains all nine different digits.

python3 -m virtualenv rt
. rt/bin/activate
pip install -r requirements.txt

Change the main_encc() at the last line of sudoku.py to main_enc().

Comment out zero or more macro definitions in define_macros keyword argument in setup.py to redefine macros in C++ implementation. Then

python setup.py build_ext -if

python sudoku.py SUDOKU_BOARD_FILE OUTPUT_FILE

An example of SUDOKU_BOARD_FILE is example-boards/board.txt.

Change

cclauses = encc.extended_encode(board)

to, e.g.,

cclauses = encc.minimal_encode(board)

in sudoku.py.

Another SAT-based sudoku solver can be found in here, which seems to use the minimal encoding as found in this repo.

• Sudoku as a SAT Problem
• A Sudoku-Solver for Large Puzzles using SAT: note on using the strategy of this paper can be found in source code c_enc.cpp.