Question: Is it possible to control some sort of preference for model return values in z3?
Example: Given the following propositional logic formula, there are 2 possible models.
a: True, b: True, c: False (preferred)a: True, b: False, c: True (still valid, just "second choice")I would like to control, via the boolean formula/assertions itself, that the model where a and b are True should have preference over the model where a and c are True. But given the case that b could not be True because additional constraints are added, the model with a and c being True should be returned.
SMT2 Formula: Here is the SMT2 example formula, which can be tested via rise4fun.
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(assert (= a true))
(assert (or
(and (= b true) (not (= c true)))
(and (= c true) (not (= b true)))
))
(check-sat)
(get-model)
Observation: I noticed that it seems actually possible to control wether or not b or c are True in the returned model, by actually switching the order of the and clauses in the or clause. Is this in some way reliable or just happening by chance for this trivial example?
This is an alternative answer, which uses the assert-soft command.
Alternative Encoding #1
I provide an encoding for OptiMathSAT first, and then explain how to modify these formulas to achieve the same result in z3. Compared with the other approach, this encoding is more suitable when there are many Boolean variables which share the same priority level, as it allows the OMT solver to use either a dedicated MaxSAT engine for each step of the lexicographic search or Cardinality Networks to enhance the standard OMT-based search.
I conflated the two toy-examples I have shown in the other answer in one incremental formula as follows:
(set-option :produce-models true)
(set-option :opt.priority lex)
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(assert (= a true))
(assert (or
(and (= b true) (not (= c true)))
(and (= c true) (not (= b true)))
))
(assert-soft a :weight 1 :id highest_priority)
(assert-soft b :weight 1 :id medium_priority)
(assert-soft c :weight 1 :id lowest_priority)
(minimize highest_priority)
(minimize medium_priority)
(minimize lowest_priority)
; First Solution
(check-sat)
(get-objectives)
(get-model)
; Second Solution
(push 1)
(assert (not (and a b)))
(check-sat)
(get-objectives)
(get-model)
(pop 1)
(exit)
This is the output:
~$ optimathsat test.smt2
sat
(objectives
(highest_priority 0)
(medium_priority 0)
(lowest_priority 1)
)
( (a true)
(b true)
(c false)
(highest_priority 0)
(medium_priority 0)
(lowest_priority 1) )
sat
(objectives
(highest_priority 0)
(medium_priority 1)
(lowest_priority 0)
)
( (a true)
(b false)
(c true)
(highest_priority 0)
(medium_priority 1)
(lowest_priority 0) )
To use this encoding with z3, it is sufficient to comment out the following three lines:
;(minimize highest_priority)
;(minimize medium_priority)
;(minimize lowest_priority)
The reason for this is that z3 implicitly defines the objective of an assert-soft command and implicitly minimizes it. Its output is:
~$ z3 test.smt2
sat
(objectives
(highest_priority 0)
(medium_priority 0)
(lowest_priority 1)
)
(model
(define-fun b () Bool
true)
(define-fun c () Bool
false)
(define-fun a () Bool
true)
)
sat
(objectives
(highest_priority 0)
(medium_priority 1)
(lowest_priority 0)
)
(model
(define-fun b () Bool
false)
(define-fun c () Bool
true)
(define-fun a () Bool
true)
)
Please note that, since z3 implicitly declares the minimization objectives for you, the assert-soft commands should appear in the same order of priority that you would like to assign to their associated objective function.
As I mentioned in the incipit, this encoding is much better than the one in the other answer in the case in which some variables share the same level of priority. To place two variables a1 and a2 at the same level of priority, you can use the same id for their assert-soft command.
For example:
(set-option :produce-models true)
(set-option :opt.priority lex)
(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const b1 Bool)
(declare-const b2 Bool)
(declare-const c Bool)
(assert (= a1 true))
(assert (or
(and (= b1 true) (not (= c true)))
(and (= c true) (not (= b1 true)))
))
(assert (or (not a1) (not a2) (not a3) ))
(assert (or (not b1) (not b2) ))
(assert-soft a1 :weight 1 :id highest_priority)
(assert-soft a2 :weight 1 :id highest_priority)
(assert-soft a3 :weight 1 :id highest_priority)
(assert-soft b1 :weight 1 :id medium_priority)
(assert-soft b2 :weight 1 :id medium_priority)
(assert-soft c :weight 1 :id lowest_priority)
(minimize highest_priority)
(minimize medium_priority)
(minimize lowest_priority)
; First Solution
(check-sat)
(get-objectives)
(get-model)
; Second Solution
(push 1)
(assert (not (and a1 b1)))
(check-sat)
(get-objectives)
(get-model)
(pop 1)
(exit)
with the output
~$ optimathsat test.smt2
sat
(objectives
(highest_priority 1)
(medium_priority 1)
(lowest_priority 0)
)
( (a1 true)
(a2 true)
(a3 false)
(b1 false)
(b2 true)
(c true)
(highest_priority 1)
(medium_priority 1)
(lowest_priority 0) )
sat
(objectives
(highest_priority 1)
(medium_priority 1)
(lowest_priority 0)
)
( (a1 true)
(a2 true)
(a3 false)
(b1 false)
(b2 true)
(c true)
(highest_priority 1)
(medium_priority 1)
(lowest_priority 0) )
Alternative Encoding #2
The interesting fact about assert-soft is that it can be used to solve lexicographic-optimization problems without any Lexicograpic-optimization engine: it is sufficient to play a bit with the weights to achieve the same result. This is what it is traditionally done in the case of SAT/MaxSAT solving. The only caveat is that one needs to place the weights carefully. Other than that, this approach might be even more efficient than the above encoding, because the entire optimization problem is solved with a single-call to the internal single-objective engine.
(set-option :produce-models true)
(set-option :opt.priority lex)
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(assert (= a true))
(assert (or
(and (= b true) (not (= c true)))
(and (= c true) (not (= b true)))
))
(assert-soft a :weight 4 :id obj) ; highest priority
(assert-soft b :weight 2 :id obj)
(assert-soft c :weight 1 :id obj) ; lowest priority
(minimize obj)
; First Solution
(check-sat)
(get-objectives)
(get-model)
; Second Solution
(push 1)
(assert (not (and a b)))
(check-sat)
(get-objectives)
(get-model)
(pop 1)
(exit)
This is the output:
~$ optimathsat test.smt2
sat
(objectives
(obj 1)
)
( (a true)
(b true)
(c false)
(obj 1) )
sat
(objectives
(obj 2)
)
( (a true)
(b false)
(c true)
(obj 2) )
I mentioned this in a comment to the other answer, but another potentially interesting solution could be to try a Bit-Vector encoding of the formula and then use the OBVBS (see "Bit-Vector Optimization" by Nadel et al.) engine for BV-optimization over a vector in which the Most Significant Bit represents the highest-priority variable and the Least Significant Bit represents the lowest-priority variable.
In case you want to give it a try, some time ago we introduced in OptiMathSAT a re-implementation of the OBVBS engine described in the paper. Z3 supports Bit-Vector optimization too.