z3 - unexpected output/not sure what output means

Question

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.

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)]

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)

Answer 1

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.

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.

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).

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}")

Output:

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