cluesbysam-solver 0.2.0

Wrapper around the Z3 SMT Solver to assist in solving CluesBySam puzzles.

'Clues by Sam' Solver

This project provides a thin wrapper around the Z3 SMT solver to assist in solving 'Clues by Sam' puzzles. Of course the whole point of such puzzles is to solve them manually, but it seemed like a nice problem to apply Z3 to. In the end the majority of this project focusses on providing an ergonomic API; the actual Z3 complexity is very low. It turns out finding a way to formalize Sam's clues can be quite fun in and of itself!

Installation

Ensure you have Z3 installed, e.g. by following the instructions in the Z3 repository. This package depends on the Z3 Python bindings, available on PyPI as z3-solver.

Then, install this package using your favorite Python package management frontend, for example:

pip install cluesbysam-solver

Usage example

This section describes a fictional 3x3 puzzle; I wouldn't want to give away the solution to any of Sam's puzzles! You can also directly read the code for the below example without intermittent explanation at example.py.

First we define a grid of people for our puzzle:

grid = (
    ('Alice', 'Bob', 'Carol'),
    ('Dave', 'Eve', 'Frank'),
    ('Grace', 'Heidi', 'Ivan'),
)

Then we initialize the solver:

from cluesbysam_solver import ClueSolver

cs = ClueSolver(grid)

The primary function we'll be using is ClueSolver.add, to add the clues as assertions for z3.

Let's assume Frank is revealed initially to be Innocent, providing the following clue: "Carol is one of my 3 criminal neighbors". We formalize this as follows:

from cluesbysam_solver import INNOCENT, CRIMINAL

p = cs.people
cs.add(p['Frank'] == INNOCENT)

# <Frank> Carol is one of my 3 criminal neighbors
cs.add(p['Carol'] == CRIMINAL)
cs.add(cs.num_criminals(cs.neighbors("Frank")) == 3)

This gives us the following output, revealing Carol's role (perhaps unsurprisingly):

... Adding clue:
Frank == 0
[+] Frank must be:      Innocent

... Adding clue:
Carol == 1
[+] Carol must be:      Criminal

... Adding clue:
0 + Heidi + Bob + Eve + Ivan + Carol == 3
[!] No new information

Now, let's assume Carol gives us the clue that "Alice only shares innocent neighbors with Grace." We first get the shared neighbors by computing the intersection of their neighbors, and then assert that they must all be innocent.

# <Carol> Alice only shares innocent neighbors with Grace
shared_neighbors = cs.neighbors("Alice") & cs.neighbors("Grace")
cs.add(cs.num_innocents(shared_neighbors) == len(shared_neighbors))

This gives us Dave and Eve;

... Adding clue:
2 - (0 + Dave + Eve) == 2
[+] Dave must be:       Innocent
[+] Eve must be:        Innocent

Dave says that "The criminals in row 1 are connected." There's a convenient function to express exactly that; by specifying the expected role and a sequence of people, we get an assertion to add.

# <Dave> The criminals in row 1 are connected
cs.add(cs.connected(CRIMINAL, cs.row(1)))

Unfortunately, it does not immediately lead to much..

... Adding clue:
And(Not(And(Bob == 0, 0 + Alice > 0, 0 + Carol > 0)),
    Not(And(Alice == 0, False, 0 + Bob + Carol > 0)),
    Not(And(Carol == 0, 0 + Bob + Alice > 0, False)))
[!] No new information

We still have Eve, though, who tells us that "There are exactly 2 innocents in column C." Using ClueSolver.column(a: str) and ClueSolver.row(i: int), we can quickly get the people in a column or row by specifying a column letter or row number.

# <Eve> There are exactly 2 innocents in column C
cs.add(cs.num_innocents(cs.column("C")) == 2)

A throve of information!

... Adding clue:
3 - (0 + Frank + Ivan + Carol) == 2
[+] Bob must be:        Criminal
[+] Heidi must be:      Criminal
[+] Ivan must be:       Innocent

Heidi's clue is "Only one row has exactly 2 innocents." That's somewhat tricky to express, but we can always rely on native Z3 functions for more complex statements. In this case, we use AtMost and AtLeast to specify that the statement ('[..] has exactly 2 innocents') pertains to a single row, without having to define which one.

You can import AtMost and AtLeast (as well as functions such as Or and Implies) directly from Z3, but cluesbysam_solver also exposes them. In this case we could have added both assertions at once using And, but can also specify them separately.

# <Heidi> Only one row has exactly 2 innocents
from cluesbysam_solver import AtMost, AtLeast

cs.add(AtMost(*(cs.num_innocents(cs.row(i)) == 2 for i in range(1, 4)), 1))
cs.add(AtLeast(*(cs.num_innocents(cs.row(i)) == 2 for i in range(1, 4)), 1))

This gives us the following.

... Adding clue:
AtMost((3 - (0 + Bob + Alice + Carol) == 2,
        3 - (0 + Dave + Eve + Frank) == 2,
        3 - (0 + Grace + Ivan + Heidi) == 2),
       1)
[!] No new information

... Adding clue:
AtLeast((3 - (0 + Bob + Alice + Carol) == 2,
         3 - (0 + Dave + Eve + Frank) == 2,
         3 - (0 + Grace + Ivan + Heidi) == 2),
        1)
[+] Grace must be:      Innocent

Ivan tells us "The number of criminals in the corners is even". Z3 does not have an Even and Odd function, but as clues involving odd and even numbers are quite common, ClueSolver provides them.

# <Ivan> The number of criminals in the corners is even
from cluesbysam_solver import Even

cs.add(Even(cs.num_criminals(cs.corners())))

And that concludes this example!

... Adding clue:
Exists(x!8, 0 + Grace + Alice + Ivan + Carol == 2*x!8)
[+] Alice must be:      Criminal

Puzzle complete! All roles have been identified!

Other functions that this example did not cover are above(person), below(person), left_of(person) and right_of(person), doing as their name suggests, as well as edges() to retrieve the people on the edges.