Pen and paper puzzles like Sudoku, Futoshiki and Skyscrapers are hugely popular. Solving such puzzles can be a trivial task for modern AI systems. However, most AI systems solve problems using a form of backtracking, while people try to avoid backtracking as much as possible. This means that existing AI systems do not output explanations about their reasoning that are meaningful to people.
Demystify is a tool which allows puzzles to be expressed in a high-level constraint programming language and uses MUSes to automatically produce descriptions of steps in the puzzle solving.
Install conjure (in conjure git checkout):
git clone https://github.com/conjure-cp/conjure && cd conjure && make && make solvers && make install
Install some python packages:
pip3 install python-sat z3-solver numpy sortedcontainers
Then try:
python3 demystify --eprime eprime/binairo.eprime --eprimeparam eprime/binairo-1.param
Demystify also has a visual interface, which you can find in a separate repository here
- Binairo
- Futoshiki
- Sudoku
- Jigsaw Sudoku
- X-Sudoku
- Miracle Sudoku
- Kakuro
- Skyscrapers
- Star Battle
- Tents and Trees
- Thermometers
- Number Hive
- Double Minesweeper
- Tridoku
All the models can be found in the eprime directory. If you are interested in a puzzle that is not implemented, there is a guide for modelling your own puzzles here.