有没有办法在 Z3py 的条件语句中添加约束？

如何解决有没有办法在 Z3py 的条件语句中添加约束？

我正在尝试使用 Z3 求解器解决子集和问题，但略有不同。子集中的总和元素应为 0，但应以不选择两个连续元素的方式选择元素。

例如：

set = [-7,-3,-2,5,8,-2]
set_len = len(set)
vars = [Int('vars_%d' % i) for i in range(set_len)]
s = Solver()
rt = []

for i in range(set_len):
    rt.append(vars[i]*set[i])
    s.add(Or(vars[i]==0,vars[i]==1))

s.add(sum(vars)>=1)
s.add(sum(rt)==0)

temp = Bool('temp')
for i in range(set_len):
    temp = vars[i] == 1
    if temp == True:
        s.add(vars[i+1]==0)

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

我面临问题的代码部分是这样的：

temp = Bool('temp')
for i in range(set_len):
    temp = vars[i] == 1
    if temp == True:
        s.add(vars[i+1]==0)

问题在于“if”条件。

我得到的解决方案之一是：

[vars_3 = 1,vars_0 = 0,vars_1 = 1,vars_4 = 0,vars_2 = 1,vars_5 = 0]

如果 vars_1 = 1，那么 vars_2 应该不等于 1。

有没有其他方法可以做到这一点？

解决方法

使用布尔值来表示选择，并确保不会同时启用两个连续的选择。类似的东西：

from z3 import *

inp  = [-7,-3,-2,5,8,-2]
pick = [Bool('pick_%d' %i) for i in range(len(inp))]

s = Solver()

# make sure we pick at least one element
s.add(Or(pick))

# make sure no consecutive elements are picked:
for i,j in zip(pick,pick[1:]):
    s.add(Not(And(i,j)))

# make sure picked elements sum to 0:
total = 0
for i,p in enumerate(pick):
    total = total + If(p,inp[i],0)
s.add(total == 0)

r = s.check()
if r == sat:
   m = s.model()
   for i,p in enumerate(pick):
       if m.eval(p): print(inp[i])
else:
    print("Solver said: %s" % r)

当我运行这个时，我得到：

-3
5
-2

满足您的约束。