如何在 Z3py 中的约束内生成条件

如何解决如何在 Z3py 中的约束内生成条件

让我们假设有 5 个时间段，在每个时间段，我有 4 个选项可供选择，每个选项都有一个已知的奖励，例如。 rewards = [5,2,1,-3]。在每个时间步，必须至少选择 4 个选项中的 1 个，条件是，如果在时间 t 选择了选项 3（奖励 -3），则对于 剩余 个时间步，不应选择任何选项。例如，考虑到选项从 0 开始索引，[2,3] 和 [2,3,99] 都是有效解，第二个解在第三个选项中选择了选项 3时间步长，99 是一些随机值，表示没有选择任何选项。

我试过的 Z3py 代码在这里：

T = 6 #Total time slots
s = Solver()

pick = [[Bool('t%d_ch%d' %(j,i)) for i in range(4)] for j in range(T)]

# Rewards of each option
Rewards = [5,-3]

# Select at most one of the 4 options as True
for i in range(T):
    s.add(Or(Not(Or(pick[i][0],pick[i][1],pick[i][2],pick[i][3])),And(Xor(pick[i][0],pick[i][1]),Not(Or(pick[i][2],pick[i][3]))),And(Xor(pick[i][2],pick[i][3]),Not(Or(pick[i][0],pick[i][1])))))

# If option 3 is picked,then none of the 4 options should be selected for the future time slots
# else,exactly one should be selected.
for i in range(len(pick)-1):
    for j in range(4):
        
        s.add(If(And(j==3,pick[i][j]),Not(Or(pick[i+1][0],pick[i+1][1],pick[i+1][2],pick[i+1][3])),Or(And(Xor(pick[i+1][0],pick[i+1][1]),Not(Or(pick[i+1][2],pick[i+1][3]))),And(Xor(pick[i+1][2],pick[i+1][3]),pick[i+1][1]))))))

if s.check()==False:
    print("unsat")
    
m=s.model()
print(m)

通过这个实现，我没有得到诸如 [2,99] 之类的解决方案。他们要么没有选项3，要么在最后一个时间段有。

我知道 If 部分中存在错误，但我无法弄清楚。是否有更好的方法来实现此类解决方案？

解决方法

很难破译你想要做什么。从对您描述的基本阅读来看，我认为这可能是 XY 问题的一个实例。有关详细信息，请参阅 https://xyproblem.info/，并尝试根据您最初的目标来提出您的问题；您正在尝试实施而不是特定的解决方案。 （在我看来，您提出的解决方案过于复杂。）

话虽如此，如果您摆脱 99 要求并简单地将 -3 指定为终止符，您就可以如所述解决您的问题。选择 -3 后，以下所有选择都应为 -3。这可以编码如下：

from z3 import *

T = 6
s = Solver()

Rewards = [5,2,1,-3]
picks = [Int('pick_%d' % i) for i in range(T)]

def pickReward(p):
    return Or([p == r for r in Rewards])

for i in range(T):
    if i == 0:
        s.add(pickReward(picks[i]))
    else:
        s.add(If(picks[i-1] == -3,picks[i] == -3,pickReward(picks[i])))

while s.check() == sat:
    m = s.model()
    picked = []
    for i in picks:
        picked += [m[i]]

    print(picked)
    s.add(Or([p != v for p,v in zip(picks,picked)]))

运行时，打印：

[5,-3,-3]
[1,5,1]
[1,1]
[2,2]
[2,5]
[2,-3]
[2,5]
...

我打断了上面的内容，因为它不断枚举所有可能的选择。在这种特殊情况下，总共有 1093 个。

（根据您的 z3 版本，您可以获得不同的答案。）

希望这可以帮助您入门。如果您有其他问题，直接说明您最初的目标通常会更有帮助。