作为解谜器的一部分，我根据用户输入动态地构建了一个图、节点和边。
每个节点被分配一个整型const，表示它是哪个连接组件的一部分。节点被限制为与其相邻节点具有相同的连接组件。
目前，它可以为多个组件分配相同的编号，但我想限制解决方案，以便每个连接的组件必须有一个唯一的编号。
我不知道如何在Z3中表达这个约束。
我不是在寻找工作代码，只是一个高层次的描述如何接近这个，我可以从那里拿它。
提前感谢!
通过其他节点连接的图组件的节点可以使用transitivecloclose建模。
下面的代码片段可能会让你开始:
# 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