I’m using z3 in python to test some graph properties according to a version a coloring problems. On a very high level, I write some constraint and when z3 fails to solve the problem it’s a graph I’m interested in.

Given:

• Nt: total number of nodes
• M: adjacency matrix
• X[i] color of node i (0 or 1)
• Nborder: number of nodes of some subgraph called border (border nodes are the Nborder first nodes)
• some constraint related to my coloring problem that are unecessary to detail here.

First I wanted to check graph where the border nodes would all have the same color. This is the list comprehension I wrote for this constraint:

const1 = [sum([X[i]*(1-X[j]) for i in range(Nborder) for j in range(Nborder) ])>=1]

aka it forces two nodes on the border to have different color. If this fail, then M forces all nodes on the border to have the same color, hence Z3 cannot solve this problem. Then I save M for later use. This line worked perfectly.

Now I want to have a look at these graphs that have the extra following property:
There’s at least two nodes of the border that have exactly two neighbors of color 1.
So I wrote this extra constraint:

const2= [sum([(sum([M[i][j]*X[j] for j in range(Nt)]) ==2) for i in range(Nborder)])<=1]

As in: the number of nodes on the border having exactly two neighbors of color 1 is at most 1.

However this produce graph that statisfies that are not what I’m looking for. How can I fix this?

I’ve heard about z3.Or() but I could not find easy to understand enough explanation about it. I tried:

s.add(z3.Or(const1, const2))

and I got:

File "/home/administrateur/.local/lib/python3.8/site-packages/z3/z3.py", line 1950, in Or
    args = _coerce_expr_list(args, ctx)
  File "/home/administrateur/.local/lib/python3.8/site-packages/z3/z3.py", line 1255, in _coerce_expr_list
    alist = [_py2expr(a, ctx) for a in alist]
  File "/home/administrateur/.local/lib/python3.8/site-packages/z3/z3.py", line 1255, in <listcomp>
    alist = [_py2expr(a, ctx) for a in alist]
  File "/home/administrateur/.local/lib/python3.8/site-packages/z3/z3.py", line 3185, in _py2expr
    _z3_assert(False, "Python bool, int, long or float expected")
  File "/home/administrateur/.local/lib/python3.8/site-packages/z3/z3.py", line 107, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Python bool, int, long or float expected

A temporary solution:
create two different solvers, s1 (including constraint const1) and s2. If both fails I am in a graph I want. It’s likely quite inefficient.