OptiMathSAT

An Optimization Modulo Theories (OMT) tool

SMT-LIBv2 Examples

These examples require OptiMathSAT version 1.3.0 or superior.

All the examples can be run like this:
~$ ./optimathsat < FILENAME.smt2

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

Set Model

; activate model generation
(set-option :produce-models true)

(declare-fun x () Int)
(assert (<= 5.5 x))

; push objective
(minimize x)

; optimize
(check-sat)

; retrieve last model
(set-model -1)
(get-model)

(exit)

Boxed Multi-Objective Optimization

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

(declare-fun x () Real)
(declare-fun y () Int)
(assert (< 72 x))
(assert (< (- 92) y))

; push multiple objectives
(minimize (+ x y))
(maximize (+ x y))

; optimize
(check-sat)

; print models
(set-model 0)
(get-model)
(set-model 1)
(get-model)

(exit)

MaxSMT

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

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

; push MaxSMT goal
; at least one constraint must be satisfied
(minimize goal :local-ub 2)

; optimize
(check-sat)

(set-model 0)
(get-model)

(exit)

MinMax

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

(declare-fun l0 () Int)
(declare-fun l1 () Int)
(declare-fun l2 () Int)

(assert (< l0 10))
(assert (< l1 12))
(assert (< l2 14))

(minmax l0 l1 l2)

(set-model -1)
(get-model)

(exit)

Lexicographic Optimization + MaxSMT Example

(set-option :produce-models true)

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

; set goal (A)
(minimize (+ (* q1 23) (* q2 21) (* q3 20) (* q4 10)))
; set goal (B)
(minimize unused_suppliers :local-lb 0 :local-ub 4)
; optimize lexicographically
(set-option :opt.priority lex)
(check-sat)
; print model
(set-model -1)
(get-model)