I am using the Z3 to optimize a cost function with some soft constraints (with weighted MaxSMT). I was curious about how the MaxSMT and the user-defined cost function interact. Does the solver minimize the MaxSMT cost and the objective function both, is there a priority mechanism? I couldn't find any documentation on this, please let me know if I missed something.
2 Answers
1
votes
A soft assertion is essentially treated as a constraint that introduces a penalty to the cost function if not satisfied:
(assert-soft F [:weight n | :dweight d ] [:id id ])- assert soft constraint F, optionally with an integral weight n or a decimal weight d . If no weight is given, the default weight is 1 (1.0). Decimal and integral weights can be mixed freely. Soft constraints can furthermore be tagged with an optional name id. This enables combining multiple different soft objectives. Fig. 1 illustrates a use with soft constraints.
So, in a sense the same MaxSMT engine handles both your general cost function and the soft-constraints in one fell swoop. The above quote and the details are in this paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf
1
votes
@alias answered the question from a technical point of view; I interpreted the question from an usability point of view, so I added an answer with a few details.
As stated by @alias, using assert-soft pushes an implicit objective function on the internal objective stack. The key point to observe is that this happens at the location in the formula of the first assert-soft statement of each group of soft-clauses with a common id <id>.
The z3 OMT solver supports 3 multi-objective combination approaches: Boxed, Lexicographic and Pareto Optimization. The last two are quite well known multi-objective optimization approaches. Boxed (a.k.a. Multi-Independent) optimization is akin to sequentially solving multiple, independent, single-objective problems having the same input formula and different cost function; only that this is done much faster in a single optimization-search swipe.
The optimization combination can be set directly within the formula, at any point in time before the call to (check-sat):
(set-option :opt.priority VALUE)
where VALUE can be either box, lex or pareto.
The multi-objective combination used by z3 by default is lexicographic optimization.
The following examples, using lexicographic optimization, showcase how the behavior of z3 changes depending on how assert-soft and minimize/maximize commands are interleaved.
Example I: All assert-soft statements appear before the minimize command. The implicit MaxSMT goal takes precedence over the LIRA goal.
(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(assert-soft (< 2 x) :weight 1 :id pb)
(assert-soft (< 2 y) :weight 1 :id pb)
(minimize (+ x y))
(check-sat)
(get-model)
(get-objectives)
results in
~$ z3 example_01.smt2
sat
(model
(define-fun y () Int
3)
(define-fun x () Int
3)
)
(objectives
(pb 0)
((+ x y) 6)
)
Example II: All the assert-soft statements appear after the minimize command. The LIRA goal takes precedence over the implicit MaxSMT goal.
(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(minimize (+ x y))
(assert-soft (< 2 x) :weight 1 :id pb)
(assert-soft (< 2 y) :weight 1 :id pb)
(check-sat)
(get-model)
(get-objectives)
results in
~$ z3 example_02.smt2
sat
(model
(define-fun y () Int
0)
(define-fun x () Int
0)
)
(objectives
((+ x y) 0)
(pb 2)
)
Example III: Interleaving of assert-soft statements with the minimize command. The implicit MaxSMT goal takes precedence over the LIRA goal.
(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(assert-soft (< 2 x) :weight 1 :id pb)
(minimize (+ x y))
(assert-soft (< 2 y) :weight 1 :id pb)
(check-sat)
(get-model)
(get-objectives)
results in
~$ z3 example_03.smt2
sat
(model
(define-fun y () Int
3)
(define-fun x () Int
3)
)
(objectives
(pb 0)
((+ x y) 6)
)
Note: other OMT solvers use different multi-objective combination defaults and handle assert-soft statements differently, so this is something to keep in mind when trying various solvers.
