我在 python 中使用 z3 根据版本和着色问题测试一些图形属性。在非常高的水平上，我编写了一些约束，当 z3 无法解决问题时，这是我感兴趣的图。 给定：
Nt：节点总数
- M：邻接矩阵
- X[i]节点i的颜色（0或1）
- Nborder：称为边界的某个子图的节点数（边界节点是Nborder第一个节点）
- 与我相关的一些约束着色问题在此无需详细说明。
- 首先我想检查图形，其中边框节点全部具有相同的颜色。这是我为此约束编写的列表理解：
又名它强制边界上的两个节点具有不同的颜色。如果失败，则 M 强制边界上的所有节点具有相同的颜色，因此 Z3 无法解决此问题。然后我保存M供以后使用。这条线工作得很好。
const1 = [sum([X[i]*(1-X[j]) for i in range(Nborder) for j in range(Nborder) ])>=1]
现在我想看看这些具有以下额外属性的图表： 边界上至少有两个节点恰好有两个颜色为 1 的邻居。 所以我写了这个额外的约束：
如：边界上恰好有两个颜色为 1 的邻居的节点数最多为 1。
const2= [sum([(sum([M[i][j]*X[j] for j in range(Nt)]) ==2) for i in range(Nborder)])<=1]
然而，这生成的图表并不满足我想要的结果。我该如何解决这个问题？
However this produce graph that statisfies that are not what I'm looking for. How can I fix this?
这个代码片段的问题在于，试图计算的约束 (const2) 的方式，即边界上恰好有两个颜色为 1 的邻居的节点数不超过 1 个。当前的实现只是检查此计数是否小于或等于 1，这对于 0 个此类节点的情况也是正确的。
为了解决这个问题，需要添加另一个约束，以确保边界上至少有两个颜色为 1 的邻居的节点数不少于 2。
以下是如何修改代码以实现此目标的方法：
# ...（现有的代码）
# 约束 1：强制边界上的两个节点具有不同的颜色
const1 = [sum([X[i]*(1-X[j]) for i in range(Nborder) for j in range(Nborder)]) >= 1]
# 约束 2：边界上恰好有两个颜色为 1 的邻居的节点数不超过 1
const2 = [sum([(sum([M[i][j]*X[j] for j in range(Nt)]) == 2) for i in range(Nborder)]) <= 1]
# 约束 3：边界上至少有两个颜色为 1 的邻居的节点数不少于 2
const3 = [sum([(sum([M[i][j]*X[j] for j in range(Nt)]) == 2) for i in range(Nborder)]) >= 2]
# 将所有约束组合在一起
constraints = const1 + const2 + const3
# ...（现有的求解器代码，使用新的“约束”列表）
通过添加
const3
，现在强制执行边界上至少有两个节点恰好有两个颜色为 1 的邻居。这应该可以解决的问题，并生成满足条件的图形。
以下是一些额外的提示：
- 验证生成的图形： 务必仔细验证 z3 生成的图形是否真的满足的所有约束条件。可以编写 Python 代码以读取邻接矩阵和颜色分配，并检查属性。
- 探索不同的约束编码： 有时可能会有多种方法使用 z3 编码相同的约束条件。如果遇到性能问题或意外结果，请尝试探索不同的编码以查看它们是否有所帮助。
- 利用 z3 的功能： z3 是一个非常强大的工具，支持各种理论和数据类型。花时间熟悉其功能，可以帮助更有效地表达约束条件和解决问题。
祝在图形属性研究中一切顺利！
标签：python,list-comprehension,z3 From： 79017839