z3-意外输出/不确定输出是什么意思

问题描述

我问a question，得到了specific answer。但是，我必须扩展此答案才能使用大量数据（下面的代码）。但是，这样做会得到我不理解的输出。

有时，我得到unsat，而有时我得到sat的{{1}}；有时s.check()和s.check()需要很长时间才能运行，而其他时间则是几秒钟。但是，我不明白的是何时获得如下输出：

s.model()

我不确定[else -> Or(Var(0) == 7,Var(0) == 13,Var(0) == 43,Var(0) == 20,Var(0) == 26,Var(0) == 16,Var(0) == 45,Var(0) == 21,Var(0) == 36,Var(0) == 5,Var(0) == 6,Var(0) == 35,Var(0) == 50,Var(0) == 28,Var(0) == 10,Var(0) == 27,Var(0) == 34,Var(0) == 14,Var(0) == 51,Var(0) == 48,Var(0) == 47,Var(0) == 19)] [else -> Or(Var(0) == 22,Var(0) == 15,Var(0) == 8,Var(0) == 24)] [else -> Or(Var(0) == 44,Var(0) == 17,Var(0) == 46,Var(0) == 11)] [else -> Or(Var(0) == 49,Var(0) == 42,Var(0) == 9,Var(0) == 31,Var(0) == 12,Var(0) == 18,Var(0) == 23,Var(0) == 34)]是什么意思，并且每组变量之间的平衡都不可用（更不用说没有变量else -> ...）。我将不胜感激任何帮助。完整代码如下。

解决方法

由于所有可变权重的总和都高于所有最大设定权重的总和，因此您的约束显然无法满足。不幸的是，总的来说，没有简单的方法可以从Z3中获得关于约束为何无法满足的解释。

与本tutorial和this book中的示例相比，当前示例似乎相当简单，即使有更多类似的约束条件，它也应可以非常快速地运行。我没有检查实现的详细信息，但是也许有些事情允许变量变高（而不是约束给定的4个集合）。在那种情况下，Z3会产生很多可能性，这些可能性会在以后的阶段中被拒绝。

要获得更一致的行为，它可能有助于在每次运行时重新启动Python。（我正在PyCharm的控制台中进行测试，每次都重新启动控制台。）

按照教程中的示例，我将解决以下约束。为了获得令人满意的示例，将4个添加到每个所需的设置大小。

in_var_list = [("var 1",4,[3]),("var 2",3,[3,5,6]),("var 3",("var 4",[4,6],["var 3"]),("var 6",("var 7",["var 4"]),("var 8",4]),("var 9",[5]),("var 10",[6],["var 9"]),("var 11",5]),("var 12",("var 13",[4]),("var 14",("var 15",("var 16",[5,("var 17",("var 18",("var 19",("var 20",["var 2"]),("var 21",["var 2","var 1"])]  # variable name,variable size,possible sets,prerequisites
in_set_list = [(3,18),(4,(5,(6,8)]  # set name,max set size


from z3 import Int,Solver,Or,And,Sum,If,sat

# add empty list to tupples of length 3
in_var_list = [tup if len(tup) == 4 else (*tup,[]) for tup in in_var_list]

print("sum of all weights:",sum([weight for _,weight,_,_ in in_var_list]))
print("sum of max weights:",sum([max_ssize for _,max_ssize in in_set_list]))


s = Solver()
v = {varname: Int(varname) for varname,*_ in in_var_list}

for name,pos_sets,prereq in in_var_list:
    s.add(Or([v[name] == p for p in pos_sets])) # each var should be in one of its possible sets
    s.add(And([v[r] < v[name] for r in prereq])) # each prerequisit should be in an earlier set
print("*** Test: adding 4 to the maximum sizes ***")
for snum,max_ssize in in_set_list:
    s.add(Sum([If(v[name] == snum,0) for name,_ in in_var_list]) <= max_ssize + 4)
    # the sum of all the weights in a set should be less than or equal to the desired size


res = s.check()
print("result:",res)
if res == sat:
    m = s.model()

    set_assignments = {name: m.evaluate(v[name]).as_long() for name,*_ in in_var_list}
    print("assignments:",set_assignments)
    for snum,desired_ssize in in_set_list:
        ssize = sum([weight for name,_ in in_var_list if set_assignments[name] == snum])
        print(f"set {snum}:",[name for name,*_ in in_var_list if set_assignments[name] == snum],f"desired size: {desired_ssize},effective size: {ssize}")

输出：

sum of all weights: 74
sum of max weights: 62

assignments: {'var 1': 3,'var 2': 4,'var 3': 3,'var 4': 4,'var 6': 5,'var 7': 5,'var 8': 3,'var 9': 5,'var 10': 6,'var 11': 3,'var 12': 4,'var 13': 4,'var 14': 3,'var 15': 5,'var 16': 5,'var 17': 5,'var 18': 4,'var 19': 3,'var 20': 6,'var 21': 6}
set 3: ['var 1','var 3','var 8','var 11','var 14','var 19'] desired size: 18,effective size: 22
set 4: ['var 2','var 4','var 12','var 13','var 18'] desired size: 18,effective size: 19
set 5: ['var 6','var 7','var 9','var 15','var 16','var 17'] desired size: 18,effective size: 22
set 6: ['var 10','var 20','var 21'] desired size: 8,effective size: 11

python z3 z3py