The OptiMathSAT OMT Solver

SMT-LIBv2 Examples

These examples require OptiMathSAT version 1.5.1 or superior.

All the examples can be run like this:

~$ ./optimathsat < FILENAME.smt2

More examples, each one including a detailed description of OptiMathSAT functionalities, can be found within OptiMathSAT binary distribution.

If necessary, in some cases you can take advantage of OptiMathSAT incrementality like this:

~$ mkfifo opti-input
~$ mkfifo opti-output
~$ ./optimathsat < opti-input > opti-output 2>&1
~$ cat > opti-input & # prevents optimathsat termination
~$ cat formula1 > opti-input
   ...read optimathsat result from opti-output...
   ...dynamically choose what formula to optimize next...
~$ cat formula2 > opti-input
   ...and so on...

BitVector Optimization

(set-option:produce-models true)
(set-option:opt.priority box)

;
; PROBLEM
;
(declare-fun x () (_ BitVec 8))
(assert (or
    (and (bvsle ((_ to_bv 8) 120) x)
         (bvsle x ((_ to_bv 8) 120))
    )
    (and (bvsle ((_ to_bv 8) 97) x)
         (bvsle x ((_ to_bv 8) 97))
    )
    (and (bvsle ((_ to_bv 8) 54) x)
         (bvsle x ((_ to_bv 8) 54))
    )
    (and (bvsle ((_ to_bv 8) 32) x)
         (bvsle x ((_ to_bv 8) 32))
    )
    (and (bvsle ((_ to_bv 8) 22) x)
         (bvsle x ((_ to_bv 8) 22))
    )
    (and (bvsle ((_ to_bv 8) 11) x)
         (bvsle x ((_ to_bv 8) 11))
    )
    (and (bvsle ((_ to_bv 8) 8) x)
         (bvsle x ((_ to_bv 8) 8))
    )
    (and (bvsle ((_ to_bv 8) (- 7)) x)
         (bvsle x ((_ to_bv 8) (- 7)))
    )
    (and (bvsle ((_ to_bv 8) (- 16)) x)
         (bvsle x ((_ to_bv 8) (- 16)))
    )
    (and (bvsle ((_ to_bv 8) (- 105)) x)
         (bvsle x ((_ to_bv 8) (- 105)))
    )
))

;
; GOALS
;
(minimize x)
(minimize x :signed)

;
; OPTIMIZATION + OPTIMUM VALUES
;
(check-sat)
(get-objectives)

(exit)

Optimization Search Bounds

(set-option :opt.priority box)

;
; PROBLEM
;
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun t () Real)

;
; GOALS
;
(minimize x)
(minimize y)
(minimize z)
(minimize t)
(maximize (+ y 1))

;
; OPTIMIZATION + OPTIMUM VALUES
;
(check-sat)
(get-objectives)

(exit)

Boxed/Multi-Independent Optimization

(set-option :opt.priority box)

;
; PROBLEM
;
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(assert (and
        (<= 42 x)
        (<= y x)
))

;
; GOALS
;
(minimize x)
(maximize y)
(maximize z)

;
; OPTIMIZATION + OPTIMUM VALUES
;
(check-sat)
(get-objectives)

(exit)

Linear Objective Combination

(set-option :produce-models true)
(set-option :opt.priority box)

;
; PROBLEM
;
(declare-fun production_cost () Real)
(declare-fun q0 () Real)           ; machine 'i' production load
(declare-fun q1 () Real) 
(declare-fun q2 () Real) 
(declare-fun q3 () Real)
(declare-fun m0 () Bool)           ; machine 'i' is used
(declare-fun m1 () Bool)
(declare-fun m2 () Bool)
(declare-fun m3 () Bool)
(assert (<= 1100 (+ q0 q1 q2 q3))) ; set goods quantity
(assert (and                       ; set goods produced per machine
    (and (<= 0 q0) (<= q0 800)) (and (<= 0 q1) (<= q1 500))
    (and (<= 0 q2) (<= q2 600)) (and (<= 0 q3) (<= q3 200))
))
(assert (and                       ; set machine `used` flag
    (=> (< 0 q0) m0) (=> (< 0 q1) m1)
    (=> (< 0 q2) m2) (=> (< 0 q3) m3)
))
(assert-soft (not m0) :id used_machines)
(assert-soft (not m1) :id used_machines)
(assert-soft (not m2) :id used_machines)
(assert-soft (not m3) :id used_machines)

;
; GOALS
; - 'total_cost' is a combination of 'production_cost'
;   and 'used_machines'
;
(minimize 
    (+ (* q0 8) (* q1 9) (* q2 9) (* q3 5)) 
    :id production_cost
)
(minimize (+ production_cost 
             (* (/ 785 10) (+ (* 2 used_machines) 8))
          )
          :id total_cost
) 

;
; OPTIMIZATION + MODEL VALUES
;
(check-sat)
(get-objectives)

(load-objective-model 1)
(get-value (total_cost))
(get-value (production_cost))

(exit)

Incremental Optimization

;
; PROBLEM
;
(declare-fun x () Real)

(push 1)
(assert (<= 5 x))
(minimize x)
(check-sat)
(get-objectives)
(pop 1)

(push 1)
(maximize x)
(check-sat)
(get-objectives)
(pop 1)

(check-sat)
(get-objectives)

(exit)

Lexicographic Optimization

(set-option :produce-models true)
(set-option :opt.priority lex)

;
; PROBLEM
;
(declare-fun cost () Real)
(declare-fun s1 () Bool)
(declare-fun s2 () Bool)
(declare-fun s3 () Bool)
(declare-fun s4 () Bool)
(declare-fun q1 () Real)
(declare-fun q2 () Real)
(declare-fun q3 () Real)
(declare-fun q4 () Real)

; set goods quantity
(assert (= 250 (+ q1 q2 q3 q4)))

; set goods offered by each supplier
(assert (or (= q1 0) (and (<= 50 q1) (<= q1 250))))
(assert (or (= q2 0) (and (<= 100 q2) (<= q2 150))))
(assert (or (= q3 0) (and (<= 100 q3) (<= q3 100))))
(assert (or (= q4 0) (and (<= 50 q4) (<= q4 100))))

; supplier is used if sends more than zero items
(assert (and (=> s1 (not (= q1 0))) (=> s2 (not (= q2 0)))
           (=> s3 (not (= q3 0))) (=> s4 (not (= q4 0)))))

; supply from the largest number of suppliers
(assert-soft s1 :id unused_suppliers)
(assert-soft s2 :id unused_suppliers)
(assert-soft s3 :id unused_suppliers)
(assert-soft s4 :id unused_suppliers)

;
; GOAL
;
(minimize (+ (* q1 23) (* q2 21) (* q3 20) (* q4 10)))
(minimize unused_suppliers)


;
; OPTIMIZATION + OPTIMUM VALUES
;
(check-sat)
(get-objectives)

(exit)

PB/MaxSMT Optimization

;
; MaxSMT Engine:
; - omt:    use OMT-based encoding & engine
; - maxres: use Maximum Resolution engine
; - ext:    use external MaxSAT solver (only via API)
;
(set-option :opt.maxsat_engine maxres)

;
; MaxSMT PROBLEM
;
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= x (- y)))
(assert-soft (< x 0) :weight 1 :id goal)
(assert-soft (< x y) :weight 1 :id goal)
(assert-soft (< y 0) :weight 1 :id goal)

;
; GOAL
;
(minimize goal)

;
; OPTIMIZATION + OPTIMUM VALUE
;
(check-sat)
(get-objectives)

(exit)

MinMax/MaxMinOptimization

(set-option :opt.priority box)

;
; PROBLEM
;
(declare-fun l0 () Int)
(declare-fun l1 () Int)
(declare-fun l2 () Int)
(assert (< 10 l0))
(assert (< 12 l1))
(assert (< 14 l2))

;
; GOAL
;
(minmax l0 l1 l2 :id my_cost)

;
; OPTIMIZATION
;
(check-sat)
(get-objectives)

(exit)

Pareto Optimization

(set-option :produce-models true)
(set-option :opt.priority pareto)

;
; PROBLEM
;
(declare-fun a () Real)
(declare-fun b () Real)
(assert (or
    (and (= a 1) (= b 1))
    (and (= a 2) (= b 1))
    (and (= a 1) (= b 2))
    (and (= a 2) (= b 2))
    (and (= a 3) (= b 1))
    (and (= a 1) (= b 3))
))

;
; GOALS
;
(maximize a)
(maximize b)

;
; INCREMENTAL OPTIMIZATION
;     3 pareto solutions
;     + unsat step
;
(check-sat)
(get-objectives)

(check-sat)
(get-objectives)

(check-sat)
(get-objectives)

(check-sat)
(get-objectives)

(exit)

Set Model

;
; ENABLE MODEL GENERATION
;
(set-option :produce-models true)

;
; PROBLEM
;
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (and
            (<= 3 x)
            (<= x 5)
))
(assert (and
            (<= 10 z)
            (<= z 20)
))
(assert (= y (+ (* 2 x) z)))

;
; GOALS
;
(minimize x)
(maximize y)

;
; BOXED OPTIMIZATION + 2 MODELS
;
(set-option :opt.priority box)
(check-sat)
(get-objectives)

;(get-model) error in box mode when multiple objectives are present

(load-objective-model 0) ; minimize x
(get-model)

(load-objective-model 1) ; maximize y
(get-model)

;
; LEXICOGRAPHIC OPTIMIZATION + 2 MODELS
;
(set-option :opt.priority lex)
(check-sat)
(get-objectives)

(get-model)

(load-objective-model 0) ; minimize x
(get-model)

(load-objective-model 1) ; maximize y
(get-model)

(exit)

OptiMathSAT

An Optimization Modulo Theories (OMT) tool