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 no

Solution 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 sizefrom z3 import Int, Solver, Or, And, Sum, If, sat

# add empty list to tupples of length 3
in_var_list = [tup iflen(tup) == 4else (*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 setprint("*** 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: 74sum 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}
set3: ['var 1', 'var 3', 'var 8', 'var 11', 'var 14', 'var 19'] desired size: 18, effective size: 22set4: ['var 2', 'var 4', 'var 12', 'var 13', 'var 18'] desired size: 18, effective size: 19set5: ['var 6', 'var 7', 'var 9', 'var 15', 'var 16', 'var 17'] desired size: 18, effective size: 22set6: ['var 10', 'var 20', 'var 21'] desired size: 8, effective size: 11