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 when I run both of the constraint, Z3 never finds a possible solution, resulting in all graphs I try being saved. I feel like I should write something as a ‘const1 or not (const1 and const2)’ constraint, but I’m quite new with z3 and I have no idea how to build such a constraint.