Z3py counting elements of a row/column up until a certain condition

Question

I am working on an SMT solver using Z3py for the game 0h_n0 for a school project. (The game can be found here 0h_n0). If you're not familiar with the game, it involves blue and red dots on a grid with the given blue dots having an integer value from 1-[grid-size]. Blue dots with a number value must "see" exactly as many blue dots within its row and column as its number value. Blue dots cannot "see" past red dots, so any blue dots behind a red dot with respect to the blue dot in question should not be counted in its "seen" value.

I'm having trouble accurately counting how many other blue dots can be seen by a given blue dot. I have a set of variables defined as:

X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(DIMENSION) ]
    for i in range(DIMENSION) ]

and an instance that looks like this:

instance = ((-1, -1, -1, 1, -1),
            (2, -1, 5, 0, -1),
            (-1, 3, 4, -1, 3),
            (1, -1, -1, 0, -1),
            (3, -1, -1, -1, 0))

Blank cells are represented by -1, Red dots by 0, and blue dots by a positive integer corresponding to the number of blue dots it should "see"

I have functions that are able to accurately determine the TOTAL number of blue dots that exist in a row or column with a given X[row][column], however, they do not account for red cells "blocking the view" of the given X[row][column].

Here is some output showing the total number of blue dots in the same column as each cell of the above instance:

 [[3, 1, 2, 0, 1],
 [2, 1, 1, 1, 1],
 [3, 0, 1, 1, 0],
 [2, 1, 2, 1, 1],
 [2, 1, 2, 1, 1]]

Note: a dot cannot "see" itself

So for example, I would like to be able to do something like this to see how many blue dots can be seen below a given X[row][column] unobstructed by red dots:

def sum_bottom(element, i, j):
        count = Sum(0, 0)
        for c in range (i+1, DIMENSION):
            if ((X[c][j])/(X[c][j]) == 0):
                break
            else:
                count = Sum(count, (X[c][j])/(X[c][j]))
        return count

However, the issue is that if ((X[c][j])/(X[c][j]) == 0) is never actually satisfied as (to the best of my understanding) (X[c][j])/(X[c][j]) is just a symbol rather than a concrete value.

Any advice on how I could approach writing this constraint in Z3py would be greatly appreciated. Let me know if there is anything unclear or if it would be helpful to show more of my code and I will provide it as needed. Cheers!

Answer 1

Fun example, and quite a good fit for SMT solvers!

In symbolic programming, you need to do the conditionals symbolically as well. That is, instead of Python's if, use z3py's If. Here's a simpler example to get you started. Let's say our array X is only one dimensional and we can only see "to our right." (i.e., each blue-cell counts those to its right, not to its left.) Some preliminaries:

from z3 import *

N = 5
X = [Int("x_%d" % i) for i in range(N)]

s = Solver()

RED = -1

In the above, I represented RED with -1, since you need to be able to tell a BLUE cell that cannot see anything else with 0. Of course, you can arrange for some other set-up as well. Also, I just declared a 1-d grid of 5 cells. Additionally, I started counting at 0, which makes programming easier, but you can start counting from 1 if you like.

Now, the idea in counting is to check if a cell is blocked and stop the count, or otherwise add the cells till you get blocked. Except, instead of stopping, we have to symbolically continue using a conditional:

def value(i):
  count     = 0
  isBlocked = False
  for c in range(i+1, N):
    count = If(isBlocked, count, If(X[c] >= 0, count+1, count))
    isBlocked = Or(isBlocked, X[c] == RED)

  return count

Note how we use If, and Or functions to see how the count should be incremented, and if we should be blocked. Otherwise, the for loop runs the entire length of the sequence starting at position i+1. You can think of this as you're summing up all possible configurations, if you like.

Now you can ask z3py what certain values of value are:

>>> value(4)
0
>>> value(3)
If(False, 0, If(x_4 >= 0, 1, 0))
>>> value(2)
If(Or(False, x_3 == -1),
   If(False, 0, If(x_3 >= 0, 1, 0)),
   If(x_4 >= 0,
      If(False, 0, If(x_3 >= 0, 1, 0)) + 1,
      If(False, 0, If(x_3 >= 0, 1, 0))))

I'll elide the output for value(1) and value(0), as they are rather large. But it's instructive to study this output and convince yourself this is the right thing to do. (And also remember that the rules I implemented are different than your original game; so it's a bit simpler. You'll have to modify accordingly.)

How do you use this? First we need to tell z3 that either a cell is RED or the value in it is equal to what the value function computes:

s = Solver()
for c in range(N):
  s.add(Or(X[c] == RED, X[c] == value(c)))

And just to make it a little interesting, let's also say we want X[3] to be a BLUE cell that can only see 1 blue cell to its right:

s.add(X[3] == 1)

Now we can compute:

>>> print(s.check())
sat
>>> m = s.model()
>>> print([m.eval(X[i], model_completion=True) for i in range(N)])
[-1, -1, 2, 1, 0]

So, z3 says a satisfying configuration is:

RED RED BLUE(2) BLUE(1) BLUE(0)

and indeed that follows the (modified) rules and the constraints we implemented above.

Once you experiment with this and get comfortable with symbolic programming in z3, see if you can extend it to 2-d and take it from there by implementing the original rules. Have fun!