CODEWITHSUNDEEP
optimizationz3smt
Jinxed
Jinxed

Reputation: 366

Restricting assert-soft to satisfiability only in optimization scenario possible?

When using mixed assert and assert-soft in optimization tasks, e.g. maximize, the soft assertions are disregarded, if they would lead to a non-optimal result.

Is it possible to restrict the "softness" to the satisfiability search only? I.e.: If the soft assertion is satisfiable at all, it is kept and then treated as "hard" assertion in the optimization?

Example exhibiting the aforementioned:

(declare-fun x () Int)
(declare-fun y () Int)

(assert (< (+ x y) (* x y)))
(assert (>= x 0))
(assert (>= y x))
;(assert-soft (>= (* 4 x) y)); x->2, y->500
(assert (>= (* 4 x) y)); x->16, y->62
(assert (<= (* x y) 1000))

(maximize (+ x y))

(set-option :opt.priority pareto)
(check-sat)
(get-value (x y (+ x y) (* x y)))
(check-sat)
(get-value (x y (+ x y) (* x y)))
;...

This would be required to fulfill the following use case:

So, given a set of user-selected (possibly conflicting) selections, the ruleset itself and finally the ratings of the set of all possible selections, one solution for all variables is to be found, which, while respecting all non-conflicting selections by the user, maximizes the total rating score.

I had the idea of using assert-soft for user selections to cancel out conflicting ones, while combining it with the optimization of z3 to get the "best" solution. However, this failed, which is the reason for this question.

Upvotes: 2

Views: 315

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

My answer is yes, if you do it incrementally.

Assume that the set of soft-clauses has only a unique Boolean assignment which makes its associated MaxSMT problem optimal.

Then, it is easy to make satisfiable soft-clauses hard by fixing the value of the associated objective function. Although z3 does not allow to put explicit constraints on the name of a soft clause group (AFAIK), one can do it implicitly by using a lexicographic multi-objective combination rather than a pareto one.

Now, in your example we can safely switch from pareto to lexicographic search because there is only one extra objective function in addition to the one implicitly defined by assert-soft. Assuming the value of the assert-soft group being fixed, the whole problem degenerates to a single-objective formula which in turn has always at-most-one Pareto-optimal solution.

Of course, this is not possible if one plans to add more objectives to the formula. In this case, the only option is to solve the formula incrementally, as follows:

(set-option:produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)

(declare-fun LABEL () Bool)
(assert (and 
    (or (not LABEL) (>= (* 4 x) y))
    (or LABEL (not (>= (* 4 x) y)))
)) ; ~= LABEL <-> (>= (* 4 x) y)
(assert-soft LABEL)

(assert (< (+ x y) (* x y)))
(assert (>= x 0))
(assert (>= y x))
(assert (>= (* 4 x) y))
(assert (<= (* x y) 1000))

(check-sat)
(get-model)
(push 1)
; assert LABEL or !LABEL depending on its value in the model

(maximize (+ x y))
; ... add other objective functions ...
(set-option :opt.priority pareto)
(check-sat)
(get-value (x y (+ x y) (* x y)))
(check-sat)
(get-value (x y (+ x y) (* x y)))
...
(pop 1)

This solves the MaxSMT problem first, fixes the Boolean assignment of the soft-clauses in a way that makes them hard, and then proceeds with optimizing multiple objectives with the pareto combination.

Note that, if the MaxSMT problem admits multiple same-weight solutions for the same optimal value, then the previous approach would discard them and focus on only one assignment. To circumvent this, the ideal solution would be to fix the value of the MaxSMT objective rather than fixing its associated Boolean assignment, e.g. as follows:

(set-option:produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun LABEL () Bool)

(assert-soft (>= (* 4 x) y) :id soft)    

(assert (< (+ x y) (* x y)))
(assert (>= x 0))
(assert (>= y x))

(assert (>= (* 4 x) y))
(assert (<= (* x y) 1000))

(minimize soft)
(check-sat)
(get-model)
(push 1)
; assert `soft` equal to its value in model, e.g.:
; (assert (= soft XXX )))

(maximize (+ x y))
; ... add other objective functions ...
(set-option :opt.priority pareto)
(check-sat)
(get-value (x y (+ x y) (* x y)))
(check-sat)
(get-value (x y (+ x y) (* x y)))
...
(pop 1)

At the time being, this kind of syntax for objective combination is supported by OptiMathSAT only. Unfortunately, OptiMathSAT does not yet support non-linear arithmetic in conjunction with optimization, so it can't be reliably used on your example.

Luckily, one can still use this approach with z3!

If there is only one extra objective function in addition to the group of soft-clauses, one can still use the lexicographic combination rather than pareto one and get the same result.

Otherwise, if there are multiple objectives in addition to the group of soft-clauses, it suffices to explicitly encode the MaxSMT problem with a Pseudo-Boolean objective as opposed to using the assert-soft command. In this way, one retains full control of the associated objective function and can easily fix its value to any number. Note, however, that this might decrease the performance of the solver in dealing with the formula depending on the quality of the MaxSMT encoding.

Upvotes: 1

Related Questions