Search code examples
logicgraph-theoryz3z3py

Z3 connected components

As part of a puzzle solver, I dynamically build a graph, nodes and edges, from user input.

Each node is assigned an integer const, representing which connected component it is part of. Nodes are restricted to have the same connected component as their neighbors.

Currently, it can assign the same number to multiple components, but I want to restrict the solution so that each connected component must have a unique number.

I cannot wrap my head around how to express this constraint in Z3.

I'm not looking for working code, just a high level description of how to approach this, and I can take it from there.

Thanks in advance!

Solution

  • Nodes of a graph component connected via other nodes can be modelled using TransitiveClosure.

    The following snippet might get you started:

    #  https://stackoverflow.com/q/56496558/1911064
from z3 import *

B = BoolSort()
NodeSort = DeclareSort('Node')

R = Function('R', NodeSort, NodeSort, B)
TC_R = TransitiveClosure(R)

s = Solver()

na, nb, nc = Consts('na nb nc', NodeSort)
s.add(R(na, nb))
s.add(R(nb, nc))
s.add(Not(TC_R(na, nc)))

print(s.check())   # produces unsat