This site uses cookies for analytics, personalized content and ads. By continuing to browse this site, you agree to this use. Learn more

Be sure to follow along with the examples by clicking the "edit" link in the corner. See what the tool says, try your own formulas, and experiment!

Z3's main functionality to checking the satisfiability of logical formulas over one or more theories. Z3 can produce models for satisfiable formulas. Yet in many cases arbitrary models are insufficient and applications are really solving optimization problems: one or more values should be minimal or maximal. When there are multiple objectives, they should be combined using Pareto fronts, lexicographic priorities, or optimized independently. This section describes a feature exposed by Z3 that lets users formulate objective functions directly with Z3. Under the hood is a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations.

The
SMT-LIB 2.0 standard
is extended with three commands for expressing optimization
objectives.
The (**maximize** *t*) command instructs **check-sat** to produce a model
that maximizes the value of term *t*.
The type of *t* must be either **Int**, **Real**, or **BitVec**.

(declare-const x Int) (declare-const y Int) (assert (< x 2)) (assert (< (- y x) 1)) (maximize (+ x y)) (check-sat) (get-objectives)

The (**minimize** *t*) command instructs **check-sat** to produce a model
that minimizes the value of term *t*.

(declare-const x Int) (declare-const y Int) (assert (< x 4)) (assert (< (- y x) 1)) (assert (> y 1)) (minimize (+ x y)) (check-sat) (get-objectives)

(declare-const x Int) (declare-const y Int) (assert (< x 2)) (assert (> (- y x) 1)) (maximize (+ x y)) (check-sat)load in editor

(declare-const x Int) (declare-const y Int) (assert (< x 4)) (assert (< (- y x) 1)) (assert (< y 1)) (minimize (+ x y)) (check-sat) (get-objectives)

(declare-const x Real) (declare-const y Real) (assert (< x 4)) (assert (< y 5)) (maximize (+ x y)) (check-sat) (get-objectives)

The (**assert-soft** *formula* **:weight** *numeral*) command asserts
a weighted soft constraint. The weight must be a positive natural number, but is optional.
If omitted, the weight is set to 1.

(declare-const x Int) (declare-const y Int) (define-fun a1 () Bool (> x 0)) (define-fun a2 () Bool (< x y)) (define-fun a3 () Bool (<= (+ y x) 0)) (assert (= a3 a1)) (assert (or a3 a2)) (assert-soft a3 :weight 3) (assert-soft (not a3) :weight 5) (assert-soft (not a1) :weight 10) (assert-soft (not a2) :weight 3) (check-sat) (get-model) (get-objectives) (eval a1) (eval a2) (eval a3)

Floating point and integer weights can be mixed; internally weights are converted into rational numbers.

load in editor(declare-const a1 Bool) (declare-const a2 Bool) (declare-const a3 Bool) (assert-soft a1 :weight 0.1) (assert-soft a2 :weight 1.0) (assert-soft a3 :weight 1) (assert-soft (or (not a1) (not a2)) :weight 3.2) (check-sat) (get-objectives) (get-model)

(declare-const x Int) (declare-const y Int) (declare-const z Int) (assert (< x z)) (assert (< y z)) (assert (< z 5)) (assert (not (= x y))) (maximize x) (maximize y) (check-sat) (get-model) (get-objectives)It is also possible to declare multiple classes of soft assertions. To do this, use an optional tag to differentiate classes of soft assertions. load in editor

(declare-const a Bool) (declare-const b Bool) (declare-const c Bool) (assert-soft a :weight 1 :id A) (assert-soft b :weight 2 :id B) (assert-soft c :weight 3 :id A) (assert (= a c)) (assert (not (and a b))) (check-sat) (get-model) (get-objectives)

(declare-const x Int) (declare-const y Int) (assert (>= 5 x)) (assert (>= x 0)) (assert (>= 4 y)) (assert (>= y 0)) (minimize x) (maximize (+ x y)) (minimize y) (set-option :opt.priority pareto) (check-sat) (get-objectives) (check-sat) (get-objectives) (check-sat) (get-objectives) (check-sat) (get-objectives)

(declare-const x Real) (declare-const y Real) (assert (>= 5 (- x y))) (assert (>= x 0)) (assert (>= 4 y)) (assert (> y 0)) (minimize x) (maximize (+ x y)) (minimize y) (maximize y) (set-option :opt.priority box) (check-sat) (get-objectives)

(declare-const x11 Bool) (declare-const x12 Bool) (declare-const x13 Bool) (declare-const x21 Bool) (declare-const x22 Bool) (declare-const x23 Bool) (declare-const x31 Bool) (declare-const x32 Bool) (declare-const x33 Bool) (declare-const y1 Bool) (declare-const y2 Bool) (declare-const y3 Bool) (define-fun bool_to_int ((b Bool)) Int (ite b 1 0) ) ; We express that a virtual machine is on exactly one server by simply converting it to integer constraints. (assert (= (+ (bool_to_int x11) (bool_to_int x12) (bool_to_int x13)) 1)) (assert (= (+ (bool_to_int x21) (bool_to_int x22) (bool_to_int x23)) 1)) (assert (= (+ (bool_to_int x31) (bool_to_int x32) (bool_to_int x33)) 1)) ; And an used server is implied by having a VM on it. (assert (and (implies y1 x11) (implies y1 x21) (implies y1 x31))) (assert (and (implies y2 x12) (implies y2 x22) (implies y2 x32))) (assert (and (implies y3 x13) (implies y3 x23) (implies y3 x33))) ; Capability constraints are quite natural to add. (assert (<= (+ (* 100 (bool_to_int x11)) (* 50 (bool_to_int x21)) (* 15 (bool_to_int x31))) (* 100 (bool_to_int y1)))) (assert (<= (+ (* 100 (bool_to_int x12)) (* 50 (bool_to_int x22)) (* 15 (bool_to_int x32))) (* 75 (bool_to_int y2)))) (assert (<= (+ (* 100 (bool_to_int x13)) (* 50 (bool_to_int x23)) (* 15 (bool_to_int x33))) (* 200 (bool_to_int y3)))) ; Optimization goals are expressed implicitly viaTheassert-softcommand. (assert-soft (not y1) :id num_servers) (assert-soft (not y2) :id num_servers) (assert-soft (not y3) :id num_servers) (assert-soft (not y1) :id costs :weight 10) (assert-soft (not y2) :id costs :weight 5) (assert-soft (not y3) :id costs :weight 20) (check-sat) (get-model) (get-objectives)

(declare-const x11 Int) (declare-const x12 Int) (declare-const x13 Int) (declare-const x21 Int) (declare-const x22 Int) (declare-const x23 Int) (declare-const x31 Int) (declare-const x32 Int) (declare-const x33 Int) (declare-const y1 Int) (declare-const y2 Int) (declare-const y3 Int) (assert (and (>= x11 0) (>= x12 0) (>= x13 0) (>= x21 0) (>= x22 0) (>= x23 0) (>= x31 0) (>= x32 0) (>= x33 0))) (assert (and (<= y1 1) (<= y2 1) (<= y3 1))) (assert (= (+ x11 x12 x13) 1)) (assert (= (+ x21 x22 x23) 1)) (assert (= (+ x31 x32 x33) 1)) (assert (and (>= y1 x11) (>= y1 x21) (>= y1 x31))) (assert (and (>= y2 x12) (>= y2 x22) (>= y2 x32))) (assert (and (>= y3 x13) (>= y3 x23) (>= y3 x33))) (assert (<= (+ (* 100 x11) (* 50 x21) (* 15 x31)) (* 100 y1))) (assert (<= (+ (* 100 x12) (* 50 x22) (* 15 x32)) (* 75 y2))) (assert (<= (+ (* 100 x13) (* 50 x23) (* 15 x33)) (* 200 y3))) (minimize (+ y1 y2 y3)) (minimize (+ (* 10 y1) (* 5 y2) (* 20 y3))) ;(set-option :opt.priority pareto) (check-sat) (get-model) (get-objectives)The capability constraints and goals are easier to express than those of boolean encoding. However, we need to add extra constraints to ensure that only 0-1 integers are allowed in the model. It is also interesting to see different results by choosing various ways of combining objectives. You can uncomment the

(set-option :smt.arith.solver 1) ; enables difference logic solver for sparse constraints (set-option :smt.arith.solver 3) ; enables difference logic solver for dense constraints (declare-const x Int) (declare-const y Int) (assert (>= 10 x)) (assert (>= x (+ y 7))) (maximize (+ x y)) (check-sat) (get-objectives)

(set-option :opt.wmaxsat_engine hsmax)Note that our implementations of these engines do not (yet) perform as well as the default on most benchmarks we have tried. The option

(set-option :opt.enable_sat true)is made available for the

(set-option :opt.elim_01 false)The Pseudo-Boolean solver is in some, often pathological, cases more efficient than using a SAT solver. For example, it handles pidgeon hole problems well. Since cutting planes are expensive, they are applied infrequently. To set their frequency use:

(set-option :smt.pb.conflict_frequency 1)The Pseudo-Boolean solver contains a few tricks. It compiles cardinality constraints and other pseudo-Boolean inequalities with small coefficients into sorting circuits. It performs this compilation on-demand, after the inequalities have been used beyond a threshold. To disable compilation use:

(set-option :smt.pb.enable_compilation false)The Pseudo-Boolean theory solver also uses dual simplex to prune infeasible branches. For constraints with many equalities and inequalities this option can be quite helpful. The option is off by default as it often incurs more overhead than benefit. To enable this option use:

(set-option :smt.pb.enable_simplex true)