Z3连接的组件

Question

作为拼图求解器的一部分，我从用户输入中动态构建图形，节点和边缘。

每个节点均分配一个整数const，代表其一部分连接的组件。 节点仅限于与邻居相同的连接组件。

当前，它可以将相同的数字分配给多个组件，但是我想限制解决方案，以便每个连接的组件必须具有唯一的数字。

我无法围绕如何在Z3中表达这种约束。

我不是在寻找工作代码，只是关于如何处理此问题的高级描述，我可以从那里进行。

提前致谢！

Answer 1

可以使用。

以下片段可能会让您入门：

#  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