有没有一种方法可以在 Z3py 的条件语句中添加约束？

Question

我正在尝试使用 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。

还有其他方法吗？

Answer 1

使用布尔值表示picks，并确保没有同时启用两个连续的picks。类似于：

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

满足你的约束。

有没有一种方法可以在 Z3py 的条件语句中添加约束？

Is there a method to add constraints within conditional statements in Z3py?

subset-sum

z3py