z3 control preference for model return values

Question

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?

How complicated is the preference order? If it's just two choices you could do two SMT calls. The first one excluding the less desirable solution. If you can express the preferences as integers or reals you can use a minimization technique to find the model with the minimum cost. I don't think that the core engine supports any kind of preference, so any solution must be built on top. — usr, Nov 25 '18 at 19:26
The preference order is always limited to 2 choices. _(Many 2 choices within the model to be precise, but they all look like in the example)_ However "external" constraints, influencing the result, can be of arbitrary complexity and count. For example there could always be an assertion like `(assert (= b false))` be thrown in the mix. Do you have an example for such minimization techniques or a link to the docs? My _(limited)_ understanding is, that as soon as an assertion like `b > c` is invalid, the model does not fall back, but the expression becomes `unsatisfiable`. — timmwagener, Nov 25 '18 at 19:35
Clearly, Patrick knows more about Z3 than I do :) A simple minimization technique is to define a loss function and add the constraint `loss <= x`. Then you successively decrease x until you get unsat. Then increase it until it is sat again. That way you can bisect to the lowest possible loss. Likely, the answers are better than this but this bisection is very simple and very general. — usr, Nov 25 '18 at 22:05
@usr provided that what you suggest to do is done *incrementally*, then it is a very nice start. Actually, some OMT solvers (e.g. OptiMathSAT), can use their own internal *binary/adaptive* search scheme if the user provides appropriate initial lower/upper bounds. Overall, depending on the number of variables, one of the two variants with the `assert-soft` encoding should perform the best, due to the very good performance of the *MaxRes* engine (see ["Maximum Satisfiability Using Core-Guided MAXSAT Resolution"](http://www.cs.toronto.edu/~fbacchus/csc2512/Lectures/2014Readings/nb_aaai2014.pdf)) — Patrick Trentin, Nov 25 '18 at 22:18
Putting all your "booleans" in a bit-vector with the most-satisfying bit as the left-most and maximizing that bit-vector value would be a good solution to this as well, morally equivalent to what @PatrickTrentin suggested, but perhaps easier to code since you only need one bit-vector variable. — alias, Nov 26 '18 at 02:10
@LeventErkok I wrote something along those lines at the end of one answer, but if you were to make a separate answer about it in detail then I would gladly upvote it. — Patrick Trentin, Nov 26 '18 at 02:24
@LeventErkok That would be appreciated. I'm actually interested in the best performing solution. Bitwise operations can sometimes do magic in that regard. Currently I'm still adapting the solution from PatrickTrentin using soft-assert for my specific use case. I want to get something functional before starting to optimize using bit magic. I'm using z3py so bit arithmetic is not something I'm dealing with on a daily basis. — timmwagener, Nov 26 '18 at 02:33

Patrick Trentin · Accepted Answer · 2018-11-25T21:59:04.473

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.

Finally ended up using the approach described as *Alternative Encoding #2*, to make it work. It's literally just a matter of assigning weights a little careful, everything else seems to just work implicitly from there on, as @Patrick Trentin described. However, performance takes quite a nosedive when using z3.Optimize, compared to just using z3.Solver without any weights. Future optimizations, either on the input data or possibly how I optimize via z3 (maybe bitvectors!?) may be needed. Anyways, thanks again for providing great help. — timmwagener, Nov 28 '18 at 18:56
@timmwagener great that works for you. If you don't mind, and there aren't licencing or other good reasons for not doing what follows, I would like to kindly ask you whether you could send the resulting set of benchmarks to `optimathsat@unitn.it`, so that we can keep track of how our tool performs over it when experimenting with new features. — Patrick Trentin, Nov 28 '18 at 20:24
Sorry for the late answer. I will check if I have permission to send you example data....however I may very well be denied. Apart from that, the performance problems, using z3py, could be avoided through an optimized soft constraint strategy using far less constraints overall that still satisfies the problem domains needs. There is now almost no difference in performance compared to using no constraints....Anyways, if I'm given permission you'll have email soon, but as mentioned I'd be surprised if that happens... — timmwagener, Dec 03 '18 at 00:14

Patrick Trentin · Answer 2 · 2018-11-25T21:35:49.397

Given an order a, b, c, ... a possible idea is to encode your toy-example in Optimization Modulo Theory, and use the lexicographic optimization 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)))
))

(maximize (ite a 1 0)) ; highest priority
(maximize (ite b 1 0))
(maximize (ite c 1 0)) ; lowest priority

(check-sat)
(get-objectives)
(get-model)

You can solve this with either z3 or OptiMathSAT, as they accept the same syntax:

~$ optimathsat test.smt2 
sat

(objectives
 ((ite a 1 0) 1)
 ((ite b 1 0) 1)
 ((ite c 1 0) 0)
)
( (a true)
  (b true)
  (c false) )

~$ z3 test.smt2 
sat
(objectives
 ((ite a 1 0) 1)
 ((ite b 1 0) 1)
 ((ite c 1 0) 0)
)
(model 
  (define-fun b () Bool
    true)
  (define-fun c () Bool
    false)
  (define-fun a () Bool
    true)
)

If you were to add a constraints that forbids the combination a /\ b 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 (not (and a b)))

(maximize (ite a 1 0))
(maximize (ite b 1 0))
(maximize (ite c 1 0))

(check-sat)
(get-objectives)
(get-model)

Then the solver(s) would find the other solution:

~$ optimathsat test.smt2 
sat

(objectives
 ((ite a 1 0) 1)
 ((ite b 1 0) 0)
 ((ite c 1 0) 1)
)
( (a true)
  (b false)
  (c true) )

~$ z3 test.smt2 
sat
(objectives
 ((ite a 1 0) 1)
 ((ite b 1 0) 0)
 ((ite c 1 0) 1)
)
(model 
  (define-fun b () Bool
    false)
  (define-fun c () Bool
    true)
  (define-fun a () Bool
    true)
)

Note 1. Please notice that I encoded the goal in the most trivial way possible, but this is not necessarily the best way to achieve the desired goal. Depending on how many variables the problem contains, and on the structure of the problem itself, then one should consider other possible encodings (e.g. use a different formulation for the objective function, use API-only features like setting branching preference over some variables, encode the problem with Bit-Vectors). Also, unless you need some SMT-specific feature, you might want to look for some SAT/MaxSAT solver with lexicographic optimization capabilities.

Note 2. In the case your notion of preference over the models is more general than the "lexicographic preference" I inferred from your toy-example, then you can still use Optimization Modulo Theories with an alternative cost function definition which suits your needs better.

Note 3. (from the comments) In case two variables a1 and a2 need to share the same priority level, then they must be placed in the same minimize/maximize directive, e.g. (maximize (+ (ite a1 1 0) (ite a2 1 0))).

Thanks for this great example! Let me run some tests using z3py, to see if it's functional for my case. 2 questions though: 1.) The order of `maximize()` definitions sets the total order used by the lexicographic optimizarion!? How exactly is that relation? 2.) What exactly does `(get-objectives)` do? It seems I can get the same result, when commenting it out [rise4fun](https://rise4fun.com/Z3/9Wslp). — timmwagener, Nov 25 '18 at 20:37
1) Yes it is a total order, no two elements have the same priority, unless they are contained in the same `maximize/minimize` command (e.g. `(maximize (+ (ite a 1 0) (ite b 1 0)))` [There are better encodings for Pseudo-Boolean goals than this. For example, in OptiMathSAT, one would use assert-soft]) 2) For `OptiMathSAT`, `(get-objectives)` results in the `(objectives ...)` part of the output. It should be the same for `z3`, unless they changed something since last time I checked. — Patrick Trentin, Nov 25 '18 at 20:42
Ok, so is it correct that if I'm just interested in an optimized model, I wouldn't need the `(get-objectives)` command, which just provides additional output? — timmwagener, Nov 25 '18 at 20:45
@timmwagener `get-objectives` prints the values of the objective functions only; This command is available even when model generation is disabled; In the case you are already printing the whole model, then you don't need it unless your objective functions are more complicated expressions; Internally, it is an extra cheap command to execute since all values are already stored in memory; — Patrick Trentin, Nov 25 '18 at 20:47
Thank you very much. I'll have some implementation/testing to do now. That will result in either more questions or an accepted/upvoted answer ;) — timmwagener, Nov 25 '18 at 20:48
You might want to way one or two days anyway, I reckon the people from z3 might want to add their own ideas on top of this first, as I am by no means an expert of their tool. — Patrick Trentin, Nov 25 '18 at 20:49

score 1 · Answer 3 · answered Nov 26 '18 at 03:44

Patrick gave a nice list of options for this one, and I think the assert-soft solution is the simplest to use. But since you asked in the comments and mentioned you also want to code using z3py, here's a solution that creates a bit-vector to contain the variables and maximizes that as one goal:

from z3 import *

noOfVars = 3
goal = BitVec('goal', noOfVars)
a, b, c = variables = Bools('a b c')

s = Optimize()
for (v, val) in zip(variables, [Extract(i, i, goal) for i in list(reversed(range(noOfVars)))]):
    s.add(v == (val == BitVecVal(1, 1)))

s.add(a)
s.add(Or(And(b, Not(c)), And(c, Not(b))))

s.maximize(goal)

print s.sexpr()
print s.check()
print s.model()

This prints:

$ python b.py
(declare-fun goal () (_ BitVec 3))
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (= a (= ((_ extract 2 2) goal) #b1)))
(assert (= b (= ((_ extract 1 1) goal) #b1)))
(assert (= c (= ((_ extract 0 0) goal) #b1)))
(assert a)
(assert (or (and b (not c)) (and c (not b))))
(maximize goal)
(check-sat)

sat
[b = True, c = False, goal = 6, a = True]

Hope this helps!

thanks for this example. I played around with it a little, but ultimately went for the much simpler solution of just assigning weights with soft-constraints. However with this approach the performance has degraded quite a bit, so I may have to revisit BitVectors for this purpose again as one possible way to improve solving performance when optimization is needed. — timmwagener, Nov 28 '18 at 19:00
Keep in mind that z3 uses different solvers when optimization is enabled, so there's definitely the cost associated by that. (Furthermore, the optimizing solver is not incremental, but maybe that doesn't matter for you.) The best "practical" trick I've seen is to utilize the multiple cores that you no doubt have: Start two copies, one with optimization and the other without; and kill the optimizing one if you get an `unsat` on the non-optimizing version. — alias, Nov 28 '18 at 19:17

z3 control preference for model return values

3 Answers3