Objective functions in Z3

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!

Introduction

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.

Optimization from the API

Z3's programmatic API exposes all available optimization features.
  • Follow this link for a tutorial on using optimization features from F#.
  • The Solver Foundation OMP format offers several convenient features for expressing optimization problems. We provide a backend to problems formulated in OMP from Codeplex
  • The Python API is also convenient for prototyping. The Optimize Python object is used when solving constraints with optimization objectives.

    • Arithmetical Optimization

    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.

    load in editor
    (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.

    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)

    Unbounded Objectives

    Not all objective functions are bounded. Z3 indicates that the maxima are at infinity, and the minima are negative infinity. load in editor
    (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)

    Tight Bounds

    Not all finite bounds can be expressed as real numbers. Bounds obtained around strict inequalities are expressed using infinitesimals. load in editor
    (declare-const x Real)
(declare-const y Real)
(assert (< x 4))
(assert (< y 5))
(maximize (+ x y))
(check-sat)
(get-objectives)

    Soft Constraints

    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.

    load in editor
    (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)

    Combining Objectives

    Many optimization problems require solving multiple objectives.

    Lexicographic Combination

    Z3 uses by default a lexicographic priority of objectives. It solves first for the objective that is declared first. load in editor
    (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)

    Pareto Fronts

    To override lexicographic priorities, set the option opt.priority to pareto. load in editor
    (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)

    Independent Objectives

    If we just want to find the optimal value for each objective, set the option opt.priority to box. load in editor
    (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)

    A Small Case Study

    In collaboration with Anh-Dung Phan.

    Problem description

    Use the problem of virtual machine placement as an example. Assume that we have three virtual machines (VMs) which require 100, 50 and 15 GB hard disk respectively. There are three servers with capabilities 100, 75 and 200 GB in that order. Find out a way to place VMs into servers in order to
  • Minimize the number of servers used
  • Minimize the operation cost (the servers have fixed daily costs 10, 5 and 20 USD respectively.)

    Boolean encoding

    We start with a boolean encoding. Let xij denote that VM i is put into server j and yj denote that server j is in use. load in editor
    (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 via assert-soft command.
(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)
    The assert-soft command represents MaxSMT which tries to maximize the weighted sum of boolean expressions belonged to the same id. Since we are doing minimization, negation is needed to take advantage of MaxSMT support.

    Integer encoding

    In this example, the boolean encoding is not really natural. Most of the constraints is of arithmetic form, it makes more sense to express them using integer arithmetic. Here is a similar encoding using integer arithmetic. load in editor
    (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 command and take a look at results.

    Advanced topics

    Difference Logic

    Z3 uses by default an implementation of dual Simplex to solve feasibility and primal Simplex for optimality. For arithmetical constraints that only have differences between variables, known as difference logic, Z3 furthermore contains alternative decision procedures tuned for this domain. These have to be configured explicitly. There is a choice between a solver tuned for sparse constraints (where the ratio of variables is high compared to number of inequalities) and a solver tuned for dense constraints. load in editor
    (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)

    Weighted Max-SAT solvers, a portfolio

    The default solver for unweighted MaxSAT problems (when all weights of the soft constraints are set to 1) is the Fu-Malik algorithm. The default solver used for weighted MaxSAT problems is called wmax. It uses a simple decision procedure that bounds weights. Several alternatives are available and they may scale better for your application. For weighted MaxSAT problems you can select the following engines wpm2 (use an implementation of the WPM2 algorithm by Ans�tegui et.al.), bcd2 (use an implementation of the bincd algorithm by Heras et.al.), pbmax (refine bounds iteratively based on Pseudo-Boolean inequalities), hsmax (use separation into solving hitting sets by Davies et.al.). To select the hsmax engine, set the option 
      (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 pbmax solver. It causes Pseudo-Boolean constraints to be compiled into propositional logic. It uses a more efficient SAT solver if the input can be compiled directly to SAT. If not, pbmax uses a custom Pseudo-Boolean theory solver. In fact, the default behavior of the optimization engine is to detect 0-1 variables from bounds constraints and use a Pseudo-Boolean solver for these. Maximization objectives over 0-1 variables are also translated to MaxSAT form such that one of the MaxSAT engines can be used. To disable this translation use 
      (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)