如何将此约束放入 Python 代码中？

Question

我正在努力使用 Z3 求解器将以下约束放入 python 代码中，但我遇到了困难。有人可以帮忙吗？

约束条件：

对于每个X，至少有一个Y
对于每个X，至多有一个Y

我尝试了下面的方法，但根据约束它是正确的，因为代码只会说：Count of x should be lower or equal to count of y。

s = z3.Solver()

x = [1,2,3,4,5,6,7,8]
y = [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]

e_count = len(x)
d_count = len(y)

s.add(d_count =< e_count)

目标是为每个 x 分配一个 y（调度问题）。

Answer 1

我不知道您的目标是什么，但您将向求解器添加布尔值，而不是函数。如果我没理解错的话，你想证明对于每个x至少有一个y。

那么您可以：

y = set(y)
for i in x:
    s.add(i in y)

Answer 2

最简单的方法是为每个 x 值分配一个自由变量（下面称为 picked），断言它在 ys 的范围内，并且确保它们是不同的。类似于：

from z3 import *

s = Solver()

xs = [1,2,3,4,5,6,7,8]
ys = [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]

# create a picked-value for each x
picked = [Int("picked_%d" % x) for x in xs]

# make sure it's within range
for p in picked:
    s.add(p >= 0)
    s.add(p < len(ys))

# make sure they're distinct
s.add(Distinct(picked))

# get a model:
r = s.check()
if r == sat:
    for (x, p) in zip (xs, picked):
       print(x, " -> ", ys[s.model()[p].as_long()])
else:
    print("Solver said:", r)

这会打印：

1  ->  1
2  ->  2
3  ->  3
4  ->  4
5  ->  5
6  ->  6
7  ->  7
8  ->  8

因此，不出所料，求解器简单地为每个 x 选择了 y 中的相同值，因为这显然满足约束条件。添加更多约束后，模型将变得更加有趣。

（请注意，x 值匹配的唯一性是由构造决定的；我们为每个 x 选择一个值，并且 Distinct 约束确保没有重复。）

如何将此约束放入 Python 代码中？

How can I put this constraint into Python code?

python

constraints

list

z3

z3py