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
.