Solving Suko with pysmt

In a waiting room this week I opened a newspaper to find the following puzzle, named “Suko” (a trademark of Puzzler).

Various approaches exist to solving them manually and it’s possible to play online. However they are an excellent candidate for an SMT solver so I decided to implement one using pysmt.

The puzzle

The idea behind Suko is simple (manually solving is not!). In the puzzle above the following requirements must be met:

• Each square must be filled with a number from 1 to 9.
• Each number can only be used once.
• There are four circles containing a number. The four adjacent (touching) squares must add up to this number.
• There are three shaded areas. The numbers in these area must add to the value given at the bottom.

These constraints can all be expressed using basic algebra and boolean logic, therefore should be possible to implement in any SMT solver.

Installing pysmt

Installing pysmt itself is trivial. A virtual environment can be used to avoid interfering with system packages. The below steps were tested on a recent Debian system.

# Create a venv
$ mkdir -p ~/venv && virtualenv ~/venv/smt

# Activate the venv
$ . ~/venv/smt/bin/activate

# Install pysmt
$ pip install pysmt

pysmt needs at least one solver to use. pysmt ships with a utility called pysmt-install to help with this. This doesn’t install within the virtual environment (it uses ~/.smt_solvers) but it doesn’t seem to pollute the system.

I picked z3 because I’d used it before, any of the supported solvers should work.

# Install the z3 solver
# You may need a compilation toolchain, on Debian ensure that `build-essential` is installed.
$ pysmt-install --z3

Finally it’s necessary to fix $PYTHON_PATH to include the directory containing the solvers. This must be done each time a new shell is used. Again pysmt-install can help, for example:

# Get the correct path, this prints the command to run
$ pysmt-install --env
export PYTHONPATH="/home/david/.smt_solvers/python-bindings-2.7:${PYTHONPATH}"

# Run this manually
$ export PYTHONPATH="/home/david/.smt_solvers/python-bindings-2.7:${PYTHONPATH}"

# .. or do it all in one step
$ source <(pysmt-install --env)

At this point you should have a working pysmt and one solver ready for use.

Making sure it works

It’s now worth trying the “hello world” example from the pysmt GitHub repository to check everything is working.

# Grab the script
$ wget https://raw.githubusercontent.com/pysmt/pysmt/master/examples/puzzle.py

# Ensure it works
$ python puzzle.py
.. the formula will be printed ..
w := 7
h := 1
d := 1
o := 9
r := 1
l := 7
e := 1

Ensure the virtual environment is activated and $PYTHON_PATH is correct if there are problems.

Implementing Suko

With the pysmt example working it’s time to play Suko.

Creating symbols

First we need a pysmt Symbol for each unknown item we are trying to find. I have labelled columns A to C and rows 1 to 3.

cells = {}
for col in ['a', 'b', 'c']:
    for row in ['1', '2', '3']:
        key = col + row
        cells[key] = Symbol(key, INT)

Note that a basic 2D array would be a “better” solution here at scale. However for a 3x3 grid a dictionary with named items makes the code easier to read.

Ensuring valid range

To ensure that each number is in the range 1..9 two constraints are needed per symbol. A GE ensures greater or equal and LE less than or equal. Without this the solver would be free to pick any integer value (negative or positive) to complete the problem.

A list comprehension can be used to do this in one line:

valid_range = And([And(GE(c, Int(1)), LE(c, Int(9))) for c in cells.values()])

This creates a list of And shortcuts for each symbol, ensuring it’s >=1 and <=9. These are combined with one And shortcut at the end.

Preventing repetition

The numbers 1 to 9 can only be used once each, repetition is not allowed. Fortunately pysmt makes this easy with the AllDifferent(..) construct:

no_repeats = AllDifferent(cells.values())

This is a shorter and cleaner way of looping through each pair of cells and adding the != logic manually (though itertools.combinations works well too).

The shaded areas

Next the three shaded areas. These need to be added up and then compared to a given figure.

The Plus(..) shortcut will add any number of values. The Equals() shortcut will test for equality. Each shaded area is implemented with a Plus (of three symbols) and one Equals to match the given value.

sum_area_1 = Equals(Plus(cells['a1'], cells['b1'], cells['b2']), Int(17))

.. repeat for two more areas ..

The circles

The circles provide the sum of four adjacent squares. Note this is identical to the shaded areas above and is expressed in the same way. A generic implementation would treat both shaded areas and the circles identically.

sum_circle_1 = Equals(
    Plus(cells['a1'], cells['a2'], cells['b1'], cells['b2']), Int(21))

.. repeat for three more circles ..

Putting it all together

Finally the overall problem can be expressed. Each constraint must be true, like so:

formula = And(valid_range, no_repeats, sum_area_1, sum_area_2,
              sum_area_3, sum_circle_1, sum_circle_2, sum_circle_3, sum_circle_4)

And this can be passed to pysmt for solving:

model = get_model(formula)
if model:
    print(model)
else:
    print("No solution found!")

A proof-of-concept script

The full script can be found in this GitHub Gist.

This takes less than a second (on a basic VM with 2 cores) and produces the following output:

$ time python suko-smt.py
((((1 <= a1) & (a1 <= 9)) & ((1 <= a3) & (a3 <= 9)) & ((1 <= a2) & (a2 <= 9)) & ((1 <= b1) & (b1 <= 9)) & ((1 <= b2) & (b2 <= 9)) & ((1 <= b3) & (b3 <= 9)) & ((1 <= c3) & (c3 <= 9)) & ((1 <= c2) & (c2 <= 9)) & ((1 <= c1) & (c1 <= 9))) & ((! (a1 = a3)) & (! (a1 = a2)) & (! (a1 = b1)) & (! (a1 = b2)) & (! (a1 = b3)) & (! (a1 = c3)) & (! (a1 = c2)) & (! (a1 = c1)) & (! (a3 = a2)) & (! (a3 = b1)) & (! (a3 = b2)) & (! (a3 = b3)) & (! (a3 = c3)) & (! (a3 = c2)) & (! (a3 = c1)) & (! (a2 = b1)) & (! (a2 = b2)) & (! (a2 = b3)) & (! (a2 = c3)) & (! (a2 = c2)) & (! (a2 = c1)) & (! (b1 = b2)) & (! (b1 = b3)) & (! (b1 = c3)) & (! (b1 = c2)) & (! (b1 = c1)) & (! (b2 = b3)) & (! (b2 = c3)) & (! (b2 = c2)) & (! (b2 = c1)) & (! (b3 = c3)) & (! (b3 = c2)) & (! (b3 = c1)) & (! (c3 = c2)) & (! (c3 = c1)) & (! (c2 = c1))) & ((a1 + b1 + b2) = 17) & ((a2 + a3 + b3) = 12) & ((c1 + c2 + c3) = 16) & ((a1 + a2 + b1 + b2) = 21) & ((b1 + c1 + b2 + c2) = 29) & ((a2 + b2 + a3 + b3) = 21) & ((b2 + c2 + b3 + c3) = 22))

c3 := 3
b3 := 2
a2 := 4
a1 := 1
b1 := 7
b2 := 9
a3 := 6
c1 := 5
c2 := 8
python suko-smt.py  0.06s user 0.01s system 94% cpu 0.076 total

The problem can clearly be seen in the logic, for example:

• (1 <= a1) & (a1 <= 9) ensures the symbol is in the range 1..9.
• (! (a2 = b1)) is repeated for each pair of symbols, ensuring each value is used once.
• A sum like ((a1 + b1 + b2) = 17) is repeated for each circle and area.

The values for each symbol are also shown. Checking these manually against the original puzzle is left as an exercise for the reader 😀

It would be trivial to expand the example script to accept a puzzle as an input, removing a lot of the duplicate code.