z3 to find minimal combinations to satisfy multiple conflicting constraints

user_9677833 0
Viewed 387

Say I have constrains: x < 2, x > 3 and x > 5, how do I get z3 to produce the minimal solutions, e.g. x = [1, 6]?

I suppose I can implement it by using Or, and block the solved condition for each solve, but that doesn't guarantee it'll produce minimal set.

My other solution is to solve each conditions individually and gather as much result as it can, and have an algorithm to select the overlapped result for every conditions.

Any idea?

z3 python
2 Answers

This sort of "tracking" constraints comes up often. While there might be multiple solutions, I think the best solution is to explicitly add tracking variables, and iterate until you have all the constraints satisfied. You should use the optimizing solver for this purpose, maximizing the number of constraints that get discharged in every call. This way you'll ensure the number of solutions remains minimal.

Based on this strategy, I'd create a tracker variable pN for each constraint, and pair them up with implication. Then, I'd maximize for the number of pN that should be satisfied. Here's a possible encoding:

from z3 import *

x = Int('x')

p1, p2, p3 = Bools('p1 p2 p3')
constraints = [(p1, x < 2), (p2, x > 3), (p3, x > 5)]

solutions = []
while constraints:
    o = Optimize()

    s = 0
    for (tracker, condition) in constraints:
        o.add(Implies(tracker, condition))
        s = s + If(tracker, 1, 0)
    o.maximize(s)

    remaining = []
    r = o.check()
    if r == sat:
        m = o.model()
        solutions.append(m[x])
        print("Candidate: %s" % m[x])
        for (tracker, condition) in constraints:
            if(m[tracker]):
                print("  Constraint: %s satisfied, skipping." % condition.sexpr())
            else:
                print("  Constraint: %s is not yet satisfied, adding." % condition.sexpr())
                remaining.append((tracker, condition))
    else:
        print("Call returned: %s" % r)
        exit(-1)

    constraints = remaining

print("Solution: %s" % solutions)

When run, this prints:

Candidate: 6
  Constraint: (< x 2) is not yet satisfied, adding.
  Constraint: (> x 3) satisfied, skipping.
  Constraint: (> x 5) satisfied, skipping.
Candidate: 0
  Constraint: (< x 2) satisfied, skipping.
Solution: [6, 0]

So, this computes the solution [6, 0]. You originally wanted [1, 6], but I believe this is a valid solution as well.

If you want to get tighter bounds as well, you can also add conditions to the optimizing solver (via minimize/maximize calls). However, this is likely to run into problems: For instance, for your original set of constraints there's no minimum/maximum value of x that satisfy them uniquely, so you can run into situations where the optimizer will fail. If you know all your variables are bounded then you can go via that route. Otherwise, you can try calling the optimizer and if it doesn't return a fixed result, go with the result of the sat call as I did above. Of course, all of this depends on the particular constraints you have, but is otherwise irrelevant to z3.

user_9363100

I think x <2, x> 3 and x> 5 have no solutions. You can find the first solution and then add it to the condition. For example

from z3 import *
solver = Solver()
x = Int('x')

constraints = [
    x < 5
]

for i in constraints:
    solver.add(i)
print(solver.check())
while solver.check() == sat:
    print(solver.model()[x])
    solver.add(x < solver.model()[x])

Output:
sat
4
0
-1
-2
-3
-4
-5
-6
-7
....
-to minus infinity

Second solution

 from z3 import *
import itertools
solver = Solver()
x = BitVec('x', 64)

combinations = [
    x < 2,
    x > 3,
    x > 5
]

#I create a list of all possible combinations of conditions
stuff = [0, 1, 2]
conditionLst = []
for L in range(0, len(stuff)+1):
    for subset in itertools.combinations(stuff, L):
        conditionLst.append(subset)
print(conditionLst)


#for every combination I am looking for solutions
for cond in conditionLst:
    solver = Solver()
    for i in cond:
        solver.add(combinations[i])
    solver.check()
    if solver.check() == sat:
        for j in cond:
            print(combinations[j], end=", ")
        print(solver.model())
    elif solver.check() == unsat:
        for j in cond:
            print(combinations[j], end=", ")
        print(solver.check())
    del solver


x < 2, [x = 1]
x > 3, [x = 4]
x > 5, [x = 6]
x < 2, x > 3, unsat
x < 2, x > 5, unsat
x > 3, x > 5, [x = 6]
x < 2, x > 3, x > 5, unsat

If there is no solution for all combinations at once, then go to the level below. If there are solutions for 2 conditions, then see if there are solutions for the third. You can make an algorithm for this.

user_142525140
Related