Solving Binary Puzzles using Python and Z3

In this article, we will be looking into how we can build a computer program for solving arbitrary Binary Puzzles using the Python programming language, and the Z3 Theorem Prover.

Z3 is a Satisfiability Modulo Theories (SMT) solver made by Microsoft Research. It is cross-platform and is released under the MIT license. Z3 comes with a Python API that we will be using. Our goal is to encode the rules of the Binary Puzzle game in terms of mathematical equations that Z3 can comprehend. Once we have defined the rules of the game for Z3, we want to use it to solve any solvable Binary Puzzle for us or tell us if the puzzle is unsolvable.

I enjoy number puzzles such as Sudoku and Binary Puzzles. For some reason, I always end up solving more Binary Puzzles than I solve Sudokus. Binary Puzzles are more straightforward than Soduku and are thus playable in a shorter amount of time. A Binary Puzzle can be played online from various websites or via applications that are available for both Android and iOS. Look in the application store on your preferred platform, and you will most likely have numerous implementations of this uncomplicated puzzle available to you. The example puzzles I use in this article are taken from BinaryPuzzle.com, which is my preferred website for playing the game in a web browser.

Let us begin by having a closer look at the Binary Puzzle game before we begin implementing the solver in the Python programming language.

Rules for Binary Puzzles

The Binary Puzzle game consists of an NxN two-dimensional game grid with some cells pre-filled with either zero or one. The rest of the cells remains empty for us to fill in with either a zero or a one. The difficulty of the game can be tuned by adding or removing pre-filled values in the initial game state.

The rules for the Binary Puzzle game are pretty simple: we must solve the puzzle using the following set of rules:

1. Each cell must contain either a zero or a one.

2. No more than two identical numbers are allowed immediately next to each other, both horizontally and vertically.

3. Each row and each column must contain an equal amount of zeros and ones.

4. Each row and each column must be unique.

An observation we can make from the third rule is that the smallest possible game grid is 2x2, and each NxN two-dimensional game grid must make use of an even N value. The 2x2 game grid is also the only size of a game grid where the second rule does not have any influence on the game, and the second rule is thus ignorable for this particularly sized game grid.

Example Game

We begin with an easy 6x6 game grid with 14 pre-filled cells out a total of 36 cells. That is 38.9% of the game grid being pre-filled for us before we have even begun. This example game will hopefully allow us to build up some intuition about the game mechanics, and make it easier for us to understand the rules we need to implement using Python and Z3 later in the article.

The initially pre-filled cells are the only cells that remain immutable throughout the game while we try to discover the value of each of the empty cells in the game grid. The pre-filled cell values are set in bold typeface in all of the visualizations in this article to make sure we do not unintentionally change any of them.

The initial game grid looks as following:

We look for the pattern where two identical numbers exist immediately next to each other either horizontally or vertically in the game grid. Once we have identified one or more identical pairs in the game grid, we know that the cells before and after the pair cannot share the same value as the pair itself because of the second rule of the game. We update the game grid with the new values:

We continue the search for patterns in the updated game grid. We have created some new locations where two identical values are in a pair, which allows us to repeat the previous step.

We can also look for a new pattern, which is when we have a horizontal or vertical triplet, where the content of the first and last cells are identical, and the middle cell is empty. Since we know from the second rule of the game that no more than two identical values are allowed immediately next to each other, we can deduct that the content of the middle cell in the triplet must be the opposite of the first and last value of the triplet. The game grid now looks as follows:

We can now fill in the remaining three cells using a mixture of the second and the third rule of the game.

Now that the game grid is complete, and no empty cells remain, we can verify that the game state satisfies each of the four rules. Each cell contains either a zero or a one. No more than two identical values are next to each other neither horizontally nor vertically. Each row and each column have an identical amount of zeros and ones. Finally, each row and column are unique.

We have solved our first Binary Puzzle manually. We can now begin building a model of the game using Python and Z3.

Building the Model

The purpose of this article is to build a Python program that can solve arbitrary Binary Puzzles for us. We use the Z3 interface for Python to do “the hard labor” of this task, but we still need to describe the game rules to the Z3 solver before it can do anything useful for us.

Before we start defining the Z3 model of the game, we need to define the representation of the game grid in Python. We use the same initial game grid as used in the example game above. In Python, we encode the game grid as follows:

puzzle = [
    [1, N, N, 0, N, N],
    [N, N, 0, 0, N, 1],
    [N, 0, 0, N, N, 1],
    [N, N, N, N, N, N],
    [0, 0, N, 1, N, N],
    [N, 1, N, N, 0, 0],
]

We represent the game grid as a list of lists of integers and N values in Python. The N value is defined as the Python value None and is used throughout this article to represent an empty cell. The task of the Z3 solver will be to eliminate any N values in the game grid and replace it with either a zero or a one.

If we were to solve the puzzles without an engine like Z3, but using “pure” Python code, the naive approach would be to define several imperative steps that try to solve the game by eliminating the empty cells one by one.

The way Z3 works is by us adding “constraints” or “assertions” that will make it possible for its built-in solver to solve the domain-specific problem that we are describing using our constraints. In this case, the Binary Puzzle game. Once we have added all of the game rules encoded as constraints to the Z3 solver, we ask it to come with a possible solution for us. Z3 will try to find a solution where all constraints are satisfied or otherwise notify us of its inability to solve the given puzzle.

To implement the Binary Puzzle solver as “bug-free” as possible, we perform some initial input validation of the input puzzle to ensure that it is meaningful before we ask Z3 to try to do anything to it. We start by defining a Python value representing the size of our game grid. We call this variable size, and we define it as follows:

size = len(puzzle)

We want to ensure that the input puzzle is non-empty:

if size == 0:
    raise InvalidPuzzleError

We want to ensure that the game grid’s size value is an even number in accordance with the observation we made while going over the rules of the game:

if size % 2 != 0:
    raise InvalidPuzzleError

We want to ensure that the NxN input puzzle has the correct dimensions, and does not contain rows or columns of a different length than N. We verify this by ensuring that each row is size cells wide:

for row in puzzle:
    if size != len(row):
        raise InvalidPuzzleError

We want to ensure that each cell in the input puzzle contains either a zero, one, or the None value since no other values are allowed:

for row in puzzle:
    for value in row:
        if value not in {0, 1, N}:
            raise InvalidPuzzleError

Now that we have validated the input puzzle to avoid the worst mistakes, we can start constructing the Z3 solver for the puzzles.

When we work with a constraint solver such as Z3, we do work with traditional programming concepts such as “variables,” but we do not assign values to them like we would in Python. Instead, we build up a set of equations that makes use of these variables, and then we ask Z3 to give us a result where all of the constraints are satisfied. If our input is impossible to solve because of violations of the game rules, Z3 will be unable to give us a solution, and the problem is considered unsatisfiable. However, if the problem is satisfiable, Z3 will have the correct value for each of our cells in the game grid.

The symbolic variables we define for Z3 has no structure, such as rows and columns. Instead, we later define the structure using the equations we add to the solver.

The first task we have to perform is to build a list of all possible x and y pairs we have in the game grid. We call these our “positions”:

positions = [
    (x, y) for x in range(size) for y in range(size)
]

We can now create the symbolic variables used by Z3. Each symbolic variable must have a name, which we in Python can represent as a string value. The string value allows us to later identify the specific variable during debugging if that becomes necessary. We create a Python dictionary of (x, y) pairs as key, and the symbolic Z3 integer as value for each cell in our game grid:

symbols = {
    (x, y): z3.Int("v{};{}".format(x, y)) for x, y in positions
}

We have now defined a symbolic variable for each cell in the 6x6 game grid. Each symbolic variable can now be looked up in our dictionary of symbols using its x and y value as the key. We also named the symbolic variables “v0;0”, “v0;1”, …, “v5;4”, “v5;5”, respectively. While we still have no structure for the symbolic variables, we can visualize the symbolic variables in the game grid in the way they will be used once we have build structure such as “rows” and “columns”:

We do not have to inform the Z3 solver about the existence of each of the symbolic variables. Instead, the solver will learn about their existence as we use them in our constraints later in the article.

The dictionary of symbols allows us to build two Python lists representing each row and each column in the game grid as lists of symbolic variables. The added structure will make it easier to implement the rules of the game in the next steps. We create the rows and columns lists in Python:

rows = []
columns = []

for x in range(size):
    row = [symbols[x, y] for y in range(size)]
    rows.append(row)

for y in range(size):
    column = [symbols[x, y] for x in range(size)]
    columns.append(column)

To avoid unnecessary duplications in our source code, we also create a variable representing both the rows and the columns in the game grid as the rules of the game often apply to both:

rows_and_columns = rows + columns

We can now instantiate the Z3 solver which we will add the constraints of the game to:

solver = z3.Solver()

Since some cells are already pre-filled for us, we need to inform Z3 about the value of these cells. We do this by adding a constraint specifying the exact value of the given symbolic variable using the equality comparison operator in Python:

for x, y in positions:
    value = puzzle[x][y]

    if value is N:
        continue

    solver.add(symbols[x, y] == value)

An important detail to understand here is that even if we apply the equality comparison operator here, the Z3 variable overloads this operator. The operator overloading ensures that it is the expression we add to the solver and not the boolean result of Python comparing the symbolic variable with the content of the value variable for equality.

Notice how we explicitly ignore the empty cells in our puzzle since the goal is to have Z3 fill those out for us.

The first set of constraints directly related to the rules of the game will be coming from the first rule: all cells in the game grid must contain either a zero or a one. We add these constraints to all of the symbolic variables in the dictionary of symbols as follows:

for symbol in symbols.values():
    solver.add(z3.Or([symbol == 0, symbol == 1]))

An example of a violation we could make now would be if our input game grid contained a value such as two, which would be a violation of the set of constraints we have added to the solver.

The next constraints we add to the Z3 solver handles the third rule of the game and ensures that each row and each column have the same amount of zeros and ones. Instead of counting each zero and one in each row and column, we encode these constraints as the sum of each row, and each column must be equal to the size divided by two:

for values in rows_and_columns:
    solver.add(z3.Sum(values) == size // 2)

The constraints needed to check the uniqueness of each row and each column are slightly more complicated but required to implement the fourth rule of the game. For each row and column, we ensure that each other row or column does not contain the same values as the current row or column does. Remember that we pass the Z3 solver symbolic variables such that the Z3 solver will check the actual content of the variables when we execute the model. We implement these constraints in Python as follows:

for lines in [rows, columns]:
    solver.add(z3.Not(z3.Or([z3.And([a == b for a, b in zip(line_a, line_b)])
                                            for line_a in lines
                                            for line_b in lines
                                            if line_a != line_b])))

The final set of constraints we need to add to the Z3 solver are only necessary for all NxN game grids where N is greater than 2. These constraints implement the second rule of the game that says no more than two identical numbers are allowed immediately next to each other horizontally and vertically.

We model these constraints using a set of “sliding windows” of three cells in each window of the game grid: each triplet must not contain three identical values in it. We can visualize the sliding window algorithm of three cells as follows:

Implementing the sliding window constraints in Python looks as follows:

if size > 2:
    for window in rows_and_columns:
        for i in range(size - 2):
            a, b, c = window[i:i + 3]
            solver.add(z3.Not(z3.And([a == b, b == c])))

Another approach we could have taken here is to check each window if the sum of the three symbolic variables is equal to 0 or 3. However, using equality checks for these constraints seemed more intuitive to the author at the time of writing this.

Using the Model

We have now implemented all the game rules as mathematical equations for Z3 to be able to solve the puzzle, but first, we have to check the solver if the current constraints are “satisfiable”. We use the solver’s check() method to achieve this:

if solver.check() != z3.sat:
    raise UnsolvablePuzzleError

If the input puzzle contained a violation of some of the constraints, such as containing two identical rows, then the call to check() would fail, and we would raise an exception.

Once we have run check() successfully, we can fetch the model that Z3 has created for the puzzle:

model = solver.model()

We can now query the model for the actual value of each of the symbolic variables stored in the dictionary of symbols. We build up a mapping between the cell positions, and the result of the evaluation of the symbolic variable:

result = {
    position: model.evaluate(symbol) for position, symbol in symbols.items()
}

We can now compute the solution of the puzzle, and put it in a data structure equivalent to the input puzzle:

solved_puzzle = [
    [result[x, y].as_long() for y in range(size)] for x in range(size)
]

If we visualize the solution from Z3, it will look as follows:

We have successfully programmed the Z3 solver such that it can solve the 6x6 game grid for us, but we implemented all of the game rules such that they will work for any NxN game grid with an even N value. We have specified the rules of the game as a set of mathematical equations instead of specifying each step Python needs to take to solve the puzzle.

It is much easier to write a validator for whether the game is correctly solved or not than it is to solve the game itself. However, we will skip the details of the validator implementation in this article.

Puzzles with Higher Difficulty

Let us have a look at how the solver handles a more difficult input puzzle. We change the input puzzle to be a 14x14 game grid instead of the example 6x6 game grid. In the new puzzle, only 45 out of 196 cells (23.0%) are pre-filled for us, making this game much harder than the example game where 38.9% of the cells were pre-filled. The new game grid looks as follows:

The Z3 solver can solve this puzzle in around 2.5 seconds on the author’s 2.6 GHz Intel i7 desktop computer from 2016. The result seems to be correct. The solution looks as follows:

Unsatisfiable Puzzles

An interesting detail that is worth including here is what happens if we ask Z3 to solve an impossible puzzle. With the rules encoded as a set of mathematical equations, we could try to build an input puzzle that passes the initial input validation but would be unsatisfiable.

One of the most trivial puzzles we can construct that is unsatisfiable and passes the input validation is this 2x2 game grid for which no possible solution exists under the rules of the game:

This game grid will be a violation of the third rule of the game whereby each row, and each column, must contain the same number of zeros and ones if we try to solve it by filling in the two empty cells. Additionally, both rows of this game would be identical, which is a violation of the fourth rule of the game. Because of these violations, this puzzle will be unsatisfiable. Passing this puzzle to the solver will make our program throw an “Unsolvable Puzzle Error” exception.

Conclusion

Exploring Z3, together with the Python programming language, has been a fun learning exercise. I could see myself use Z3 to solve various real-world problems that I have historically relied on implementing manual solutions crafted by hand to solve. Changing my mindset from trying to solve the specific problem by hand over to modeling the problem in a declarative way is entertaining and something I wish I could make use of more often in my daily life as a programmer.

If you are interested in learning more about using Z3 together with the Python programming language, I suggest you take a look at the excellent Programming Z3 guide by Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, and Christoph Wintersteiger from Microsoft Research.

The source code for the Binary Puzzle solver, we implemented in this article, is available from Github. The source code is published under the BSD 2-Clause license.