Search code examples
pythonz3z3py

Find maximum value of a variable given constraints in z3py

For example, given the following 4 constraints, a and x are ints, b is array, maps int to int: 

a >= 0
b[0] == 10
x == 0
b[x] >= a

find_max(a) => 10
find_min(a) => 0

Can z3py do something like this?

Solution

  • Yeah, sure.

    You can either do it incrementally, via multiple single-objective optimization searches, or use the more efficient boxed (a.k.a. Multi-Independent) combination offered by z3 for dealing with multi-objective optimization.

    Definition 4.6.3. (Multiple-Independent OMT [LAK+14, BP14, BPF15, ST15b, ST15c]). Let <φ,O> be a multi-objective OMT problem, where φ is a ground SMT formula and O = {obj_1 , ..., obj_N}, is a sorted list of N objective functions. We call Multiple-Independent OMT problem, a.k.a Boxed OMT problem [BP14, BPF15], the problem of finding in one single run a set of models {M_1, ...,M_N} such that each M_i makes obj_i minimum on the common formula φ.

    Remark 4.6.3. Solving a Multiple-Independent OMT problem <φ, {obj_1, ..., obj_N }> is akin to independently solving N single-objective OMT problems <φ, obj_1>, ..., <φ, obj_N>. However, the former allows for factorizing the search and thus obtaining a significant performance boost when compared to the latter approach [LAK+14, BP14, ST15c].

    [source, pag. 104]

    Example:

    from z3 import *

a = Int('a')
x = Int('x')
b = Array('I', IntSort(), IntSort())

opt = Optimize()

opt.add(a >= 0)
opt.add(x == 0)
opt.add(Select(b, 0) == 10)
opt.add(Select(b, x) >= a)

obj1 = opt.maximize(a)
obj2 = opt.minimize(a)

opt.set('priority', 'box')   # Setting Boxed Multi-Objective Optimization

is_sat = opt.check()
assert is_sat

print("Max(a): " + str(obj1.value()))
print("Min(a): " + str(obj2.value()))

    Output:

    ~$ python test.py 
Max(a): 10
Min(a): 0

    See publications on the topic like, e.g.

    1. Nikolaj Bjorner and Anh-Dung Phan. νZ - Maximal Satisfaction with Z3. In Proc International Symposium on Symbolic Computation in Software Science, Gammart, Tunisia, December 2014. EasyChair Proceedings in Computing (EPiC). [PDF]

    2. Nikolaj Bjorner, Anh-Dung Phan, and Lars Fleckenstein. Z3 - An Optimizing SMT Solver. In Proc. TACAS, volume 9035 of LNCS. Springer, 2015. [Springer] [[PDF]