[Python] Using z3 to find graphs not conforming to property A and property B

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 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*(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[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.

Continue reading...