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

Question

让我们假设有 5 个时间段，在每个时间段，我有 4 个选项可供选择，每个选项都有一个已知的奖励，例如。 rewards = [5, 2, 1, -3]。在每个时间步，必须至少选择四个选项中的一个，条件是，如果在时间 t 选择了选项 3（奖励为 -3），则剩余时间步长，应选择 none 个选项。例如，考虑到选项从 0 开始索引，[2, 1, 1, 0, 3] 和 [2, 1, 1, 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, 2, 1, -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]), Not(Or(pick[i+1][0], pick[i+1][1]))))))

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

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

我知道 If 部分有错误，但我无法弄清楚。有没有更好的方法来实现这样的解决方案？

Answer 1

很难理解您要做什么。从您的描述的基本阅读来看，我认为这可能是 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, -3, -3, -3]
[1, 5, 5, 5, 5, 1]
[1, 2, 5, 5, 5, 1]
[2, 2, 5, 5, 5, 1]
[2, 5, 5, 5, 5, 1]
[2, 1, 5, 5, 5, 1]
[1, 1, 5, 5, 5, 1]
[2, 1, 5, 5, 5, 2]
[2, 5, 5, 5, 5, 2]
[2, 5, 5, 5, 5, 5]
[2, 5, 5, 5, 5, -3]
[2, 1, 5, 5, 5, 5]
...

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

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

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

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

How to generate conditions within constraints in Z3py

z3

z3py