Combining Objectives

Many optimization problems require solving multiple objectives.

Lexicographic Combination

Z3 uses by default a lexicographic priority of objectives. It solves first for the objective that is declared first.

It is also possible to declare multiple classes of soft assertions. To do this, use an optional tag to differentiate classes of soft assertions. The first tag group A is given precedence over the second group B that is introduced later.

Pareto Fronts

To override lexicographic priorities, set the option opt.priority to Pareto.

Independent Objectives

If we just want to find the optimal value for each objective, set the option opt.priority to box.