我正在努力使用 Z3 求解器將以下約束放入 python 代碼中，但我很難。有人可以幫忙嗎？
約束：
- 對于每個 X 至少有一個 Y
- 對于每個 X 最多有一個 Y
我嘗試了下面的方法，但根據約束它是正確的，因為代碼只會說：x 的計數應該低于或等于 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 分配 ay（調度問題）。
uj5u.com熱心網友回復：
最簡單的方法是picked為每個x值分配一個自由變數（下面稱為），斷言它在 的范圍內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約束確保沒有重復。）
uj5u.com熱心網友回復：
我不知道您的目標是什么，但您將為求解器添加布林值，而不是函式。如果我理解正確，您想證明對于每個 x 至少有一個 y。
那么你就可以：
y = set(y)
for i in x:
s.add(i in y)
轉載請註明出處，本文鏈接：https://www.uj5u.com/ruanti/430314.html