A Playground for testing our SMT's python bindings, learning tkinter, solving Sudoku puzzles, trying to give hints, and delving into the intracies of generating sudoku puzzles, measuring their difficulty, and the list goes on.
The tool is in a pretty good state. Play with it. Let me know what else it needs, or needs explaining.
You need a newish Python, I quite like and make use of the new format strings, so you will need at least 3.6.
The software is packaged as a pip package, but to install it successfully you will first need to install yices which can be done by building from source, or using apt on linux (from our PPA) or homebrew on a mac, the README.md there describes the process.
So you can either do
pip install sudokusensei
or if you want to hack, clone this repository and do
make develop
There is a make file that will build and install the package. Once installed, you start of with an empty board
sudokusensei
If you press the options button you will be able to load one of our many predefined boards in the data directory, and you can also directly launch one of these via
sudokusensei --board <board base name>
For example:
sudokusensei --board sofa
will start you off with the puzzle that Daniel Beer (@dlbeer) mentions in showing the difference in difficulty between sofa and non-sofa search, see the references below.
Another example would be
sudokusensei --board hardest
which will start you off with the puzzle that Finnish mathematician Arto Inkala claimed is the hardest one possible, see the screen shot above.
Once you have the puppy up you can always generate new puzzles. The options tab will allow you to attempt to specify the level of difficulty of the generated puzzle.
You can even use the tool to create your own Sudoku puzzles, just start with an empty board, and make use of the Show > # Solutions
feature to make sure your puzzle has a unique solution. You can save it from the options tab.
The tool can do lots of things. Instead of writing a well structured guide, I am going to just list the features as they occur to me. Sorry.
You can make notes by simply entering multiple numbers, the same number entered twice will toggle that number in or out.
If you are really lazy you can start off your notes from the freedom analysis (Show > Freedom Notes).
You can see if you are on the right track by pressing the Check button. The UI is in a primitive state, and maybe
I will get around to highlighting the wrong squares rather than just naming them.
The freedom analysis assigns to each empty cell the set of legal possibilities for that cell. I.e. choices that do
not obviously violate the uniqueness axioms.
You can look at the freedom analysis of the puzzle via Show > Freedom, and get rid of them via
Clear > Freedom.
As the most primitve kind of hint, one can ask for the least free cell via Show > Least Free which will highlight
the cell with the smallest freedom set.
You can ask for a hint. Hints are hard. What we do is compute the minimal unsat core for each empty cell (with
some optimizations: see the cutoff in the options tab) and point out a cell with the smallest such core. This is usually a good indication that
the cell can be solved relatively easily by a human. Though of course with really hard puzzles these are still really hard
to solve. If you turn on debugging via the options tab, you will even see (in the console) the actual answer. But don't cheat, you won't feel better for it.
A legal puzzle should have exactly one solution, but when you are designing your own you may have many solutions.
You can count the number of solutions via Show > # Solutions. This computation could take a long time, so we have
a simple upper bound cutoff called aleph_nought that you can configure in the options tab.
Estimating the difficulty of a puzzle is also hard. We provide three, two are branch-difficulty measures of two
different backtracking solution search algorithms presented in [3].
These are somewhat adhoc in congruent puzzles (via the natural symmetries) will have different difficulties.
Show > Difficulty (No Sofa) and Show > Difficulty (Sofa) give these values (ranging from 0 to above 1000).
We also present another metric (that we cooked up) but this takes time to compute, so be patient. It
is a metric, and is basically proportional to the sum of the sizes of all the minimal unsat cores. This is
computationally expensive to calculate, but does provide me with a good example for which to use threads and
thread safe yices, so I will probably spend some more time on this in the not to distant future.
Generating difficult puzzles quickly is difficult.
We again rely on the earlier work of Daniel Beer.
To generate a new puzzle just press the New button.
The options tab has several parameters that affect what happens under the
hood once this button is pressed. You can choose the language (C or Python)
in which the search takes place, the tye of search algorithm used (Sofa or No Sofa).
The target difficulty, and how long one searches for a suitable puzzle.
Not all the Python options have been implemented (In particular Sofa search). But
there is not much coding left.
Warning using Python as the language requires patience, and being in debug mode is good, so one can see the progress being made.
You can solve the current puzzle by just pressing the Solve button. This uses the SMT solver, rather than the
two other techniques. Solving is easy, so not much to say here.
This project was built on top of the nice python tutorial [2] by @econchic who is hereby thanked. The tutorial is under the creative commons license which does not appear to be an option in GitHub's license widget, consequently I choose the nearest one I could, if this is a problem let me know.