python - 在 bool 列表上创建或约束

Question

我正在 Python 中使用 Z3 来生成溶解难题的解决方案。我之前没有 SAT/SMT 求解器或 Z3 的经验，甚至我的 Python 仍处于洋泾浜水平。所以请温柔一点。

在我的方法中，我有两个 bool 值列表 xs 和 ys。我从其他约束中知道，在两个列表中的每一个中，最多有一个条目为 True，而所有其他条目均为 False。每个列表零个或一个 True 条目。

我想添加一个约束来比较两个列表是否都具有 True 条目或都为 False。

所以我想要类似 or(all_the_xs)==or(all_the_ys) 的东西。我有一种感觉，这应该是 Z3 的原生特性，但我不知道如何表述。

我设法通过使用z3.Sum([z3.If(x,1,0) for x in xs])比较真实值的计数来做到这一点但这确实超出了简单 bool 值的范围。它还感觉不优雅且效率较低。

这是我的 bodged 代码的一个具有代表性的独立示例，使用 Sum() :

import z3

solver = z3.Solver()

xs = [ z3.Bool("x_{i}".format(i=i)) for i in range(0,10) ]
ys = [ z3.Bool("y_{i}".format(i=i)) for i in range(0,10) ]

xsum = z3.Sum([z3.If(x,1,0) for x in xs])
ysum = z3.Sum([z3.If(x,1,0) for x in ys])

solver.add(xsum == ysum)

solver.check()
print(solver.model())

你能帮我以更漂亮、更适合 Z3 的形式重申这一点吗？或者向我保证这样就可以了？

感谢您的阅读和思考，玛丽安

Answer 1

你很幸运! z3py 带有 Or，它采用 bool 值列表:

import z3

solver = z3.Solver()

xs = [ z3.Bool("x_{i}".format(i=i)) for i in range(0,10) ]
ys = [ z3.Bool("y_{i}".format(i=i)) for i in range(0,10) ]

solver.add(z3.Or(xs) == z3.Or(ys))

solver.check()
print(solver.model())

打印:

[x_0 = False,
 x_1 = False,
 x_2 = False,
 x_3 = False,
 x_4 = False,
 x_5 = False,
 x_6 = False,
 x_7 = False,
 x_8 = False,
 x_9 = False,
 y_0 = False,
 y_1 = False,
 y_2 = False,
 y_3 = False,
 y_4 = False,
 y_5 = False,
 y_6 = False,
 y_7 = False,
 y_8 = False,
 y_9 = False]

不是最有趣的模型，但我相信这正是您正在寻找的!