z3 - 意外输出/不确定输出意味着什么 [英] z3 - unexpected output/not sure what output means

问题描述

我问了一个问题并得到了一个具体答案.但是，我不得不扩展这个答案以处理大量数据(下面的代码).但是，这样做时，我得到了一个我不明白的输出.

I asked a question and got a specific answer. However, I had to extend this answer to work with a large set of data (code below). However, in doing so, I get an output that I do not understand.

有时，我得到一个unsat，有时我得到一个sat s.check()；有时 s.check() 和 s.model() 需要很长时间才能运行，而其他时间则是几秒钟.但是，我不明白的是当我得到这样的输出时:

Sometimes, I get a unsat and other times I get a sat for s.check(); sometimes the s.check() and s.model() take very long to run and other times, seconds. However, what I do not understand is when I get output like this:

[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 ->... 表示每个集合中变量的平衡是关闭的(更不用说没有变量44).我将不胜感激任何帮助.完整代码如下.

I'm not sure what the else -> ... means and the balance of variables in each set is off (not to mention there is no variable 44). I would appreciate any help. The full code is below.

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

in_set_list = [(3, 18), (4, 18), (5, 18), (6, 18)]
            #set name, max set size

from z3 import *

s = Solver()

allElems = {vari[0]: Int(vari[0]) for vari in in_var_list}
s.add(Distinct(list(allElems.values())))

#Python 3.6 - dictionaries are ordered
#split into sets
allSets = {c_set[0]: Const(str(c_set[0]), SetSort(IntSort())) for c_set in in_set_list}

#Generic requirement: Every element belongs to some set:
for e in allElems.values():
    belongs = False;
    for x in allSets.values():
        belongs = Or(belongs, IsMember(e, x))
    s.add(belongs)

#capacity requirements
for c_set in in_set_list:
  c_set_size = Int(c_set[1])
  s.add(SetHasSize(allSets[c_set[0]], c_set_size))
  s.add(c_set_size <= c_set[1])

#vari set requirements
for vari in in_var_list:
  set_mem_list = []
  for c_set in vari[2]:
    set_mem_list.append(IsMember(allElems[vari[0]], allSets[c_set]))
  s.add(Or(set_mem_list))

#pre-set requirements
vari_dict = {vari[0]: vari for vari in in_var_list}
for vari in in_var_list:
  try: #may not include preset
    for prereq in in_var_list[3]:
      for i, c_set in enumerate(in_set_list):
        if c_set[0] in vari_dict[prereq][2]:
          imps = []
          for subc_set in in_set_list[i+1:]:
            imps.append(IsMember(allElems[vari[0]], allSets[subc_set]))
          s.add(Implies(IsMember(allElems[prereq], allSets[c_set[0]], Or(imps))))
          s.add(Not(IsMember(allElems[prereq], allSets[in_set_list[-1]])))
  except:
    pass

r = s.check()
print(r)
if r == sat:
  modout = s.model()
else:
  raise ValueError('unsat - too many constraints, cannot fit all variables as given')

vari_out = {modout[allElems[vari]]: vari for vari in allElems}
print(vari_out)

set_out = dict()
for s in allSets:
  set_out[s] = modout[allSets[s]].as_list()

rets = dict()
for s in allSets:
  rets[s] = []
  for c in (set_out)[s][0].children():
    try:
      rets[s].append(vari_out[c.children()[1]])
    except:
      pass
print(rets)

"""# print results"""

from pprint import pprint
pprint(rets)

推荐答案

您的约束显然是不可满足的，因为所有变量权重的总和高于所有最大设置权重的总和.不幸的是，一般来说，没有简单的方法可以从 Z3 中获得关于约束不可满足的原因的解释.

Your constraints are clearly unsatisfiable, as the sum of all variable weights is higher than the sum of all maximum set weights. Unfortunately, in general there is no easy way to obtain an explanation from Z3 for why constraints are unsatisfiable.

与本教程和这本书，当前的例子看起来相当简单，它应该运行得非常快，即使对于更多类似的约束.我没有检查你的实现细节，但也许有些东西允许变量变得非常高(而不是限制到 4 个给定的集合).在这种情况下，Z3 会产生许多在稍后阶段被拒绝的可能性.

Compared to the examples in this tutorial and this book, the current example seems rather simple, and it should run quite quickly, even for many more similar constraints. I didn't check the details of your implementation, but maybe something allows the variables to get very high (instead of being constraint to the 4 given sets). In that case Z3 would generate many possibilities that are rejected in a later stage.

为了获得更一致的行为，每次运行都重新启动 Python 可能会有所帮助.(我在PyCharm的控制台测试，每次都重启控制台)

To get a more consistent behavior, it could help to restart Python for every run. (I am testing in the console of PyCharm, and restart the console each time).

按照教程中的示例，我将解决如下约束.为了获得可满足的示例，每个所需的集合大小都加上 4.

Following the examples at the tutorial, I would tackle the constraints as follows. To obtain a satisfiable example, 4 is added to each of the desired set sizes.

in_var_list = [("var 1", 4, [3]), ("var 2", 3, [3, 4, 5, 6]), ("var 3", 3, [3, 4, 5, 6]), ("var 4", 4, [4, 5, 6], ["var 3"]), ("var 6", 4, [4, 5, 6], ["var 3"]), ("var 7", 3, [4, 5, 6], ["var 4"]), ("var 8", 3, [3, 4]), ("var 9", 3, [5]), ("var 10", 3, [6], ["var 9"]), ("var 11", 4, [3, 5]), ("var 12", 4, [3, 4, 5, 6]), ("var 13", 4, [4]), ("var 14", 4, [3]), ("var 15", 4, [5]), ("var 16", 4, [5, 6]), ("var 17", 4, [3, 4, 5, 6]), ("var 18", 4, [3, 4, 5, 6]), ("var 19", 4, [3, 4, 5, 6]), ("var 20", 4, [4, 5, 6], ["var 2"]), ("var 21", 4, [5, 6], ["var 2", "var 1"])]  # variable name, variable size, possible sets, prerequisites
in_set_list = [(3, 18), (4, 18), (5, 18), (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, weight, 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, weight, 0) for name, weight, _, _ 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, weight, _, _ 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

这篇关于z3 - 意外输出/不确定输出意味着什么的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！