在布尔列表上创建或约束

Question

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

在我的方法中，我有两个布尔值列表 xs 和 ys。我从其他约束中知道，在两个列表中的每一个中，最多一个条目是 True，而所有其他条目都是 False。每个列表有 0 个或 1 个 True 条目。

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

所以我想要or(all_the_xs)==or(all_the_ys) 之类的东西。我觉得这应该是 Z3 的原生语言，但我不知道该怎么说。

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

这是我使用 Sum() 的 bodged 代码的一个有代表性的自包含示例：

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，它接受一个布尔列表：

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]

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