我问了一个问题，得到了一个具体的答案。然而，我不得不将这个答案扩展到使用大量数据(下面的代码(。然而，在这样做的过程中，我得到了一个我不理解的输出。
有时，我得到一个unsat，而其他时候，我得到s.check()的sat；有时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 -> ...是什么意思，每组变量的平衡都不平衡(更不用说没有变量44(。如果有任何帮助，我将不胜感激。完整的代码如下。
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中获得约束不可满足的原因的解释。
与本教程和本书中的示例相比，当前的示例似乎相当简单，即使在有更多类似约束的情况下，它也应该运行得很快。我没有检查您实现的细节，但可能有一些东西允许变量变得非常高(而不是限制在4个给定的集合中(。在这种情况下，Z3将产生许多在稍后阶段被拒绝的可能性。
为了获得更一致的行为，每次运行都重新启动Python可能会有所帮助。(我在PyCharm的控制台中进行测试，每次都会重新启动控制台(。
根据教程中的示例，我将处理以下约束。为了获得令人满意的示例，将4添加到每个期望的集合大小。
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