时间戳

首页 > 解决方案 > 有没有一种方法可以在 Z3py 的条件语句中添加约束？

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)

问题在于“如果”条件。

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

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

如果 vars_1 = 1，则 vars_2 不应等于1。

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

标签： z3pysubset-sum

解决方案

使用布尔值来表示选择，并确保没有同时启用两个连续的选择。就像是：

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

满足您的约束。

推荐阅读