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?

Answer 1

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.

Answer 2

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))).

Answer 3

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!