OptiMathSAT

Note: OptiMathSAT now requires -optimization=true to be set in order to use the optimization interface. If that option is not set, OptiMathSAT behaves as MathSAT.

OptiMathSAT (>= 1.7.0) accepts a modified version of SMT-LIBv2 input format, extended as follows:

• An option to configure optimathsat to optimize in lexicographic, pareto or boxed mode when dealing with multiple objectives:

    ; set boxed or lexicographic optimization
  (set-option :opt.priority box|lex|pareto)
  



• A pair of commands to set a linear arithmetic term as a new objective:

    ; push min(TERM)
    ; on the stack of objectives
  (minimize <TERM>
                   :signed
                   :id label)
  
    ; push max(TERM)
    ; on the stack of objectives
  (maximize <TERM>
                   :signed
                   :id label)
  

  Notes:
  • The (optional) signed flag is only used to mark a BV objective as signed
  • The (optional) id is useful for combining objectives or retrieving the model value


• A pair of commands to define MinMax or MaxMin objectives over a list of linear arithmetic terms:

    ; push min(max(TERM_0), ..., max(TERM_N))
    ; on the stack of objectives
  (minmax <TERM_0> ... <TERM_N>
                     :signed
                     :id label)
  
    ; push max(min(TERM_0), ..., min(TERM_N))
    ; on the stack of objectives
  (maxmin <TERM_0> ... <TERM_N>
                     :signed
                     :id label)
  

  Notes:
  • The (optional) signed flag is only used to mark a BV objective as signed
  • The (optional) id is useful for combining objectives or retrieving the model value


• A command to specify soft clauses for MaxSMT:

    ; Associate a cost weight to not satisfying TERM 
    ; the equation of cost MAXSMT_GROUP
  (assert-soft <TERM> :weight WEIGHT
                      :id MAXSMT_GROUP)
  

  Notes:
  • if :weight is omitted, it is assumed to be 1
  • WEIGHT must be a constant-valued TERM of Real or Integer type
  • if MAXSMT_GROUP is omitted, the cost is puhed inthe default group "I"
  • In order to activate the MaxSMT group, the user should explicitly use the MAXSMT_GROUP label within an objective to be minimized.


• A command to load into OptiMathSAT environment the optimum model of a cost function:

    ; load into memory the optimum model of the
    ; objective at position N%size(objective_stack)
    ; N can be positive, negative or zero.
  (load-objective-model <INT>)
  

  Notes:
  • it can not be used when there are no objectives


• A command to print the value of all objectives on the stack of objectives:

  (get-objectives)
  

The input problem must be given to OptiMathSAT on standard input:

~$ ./optimathsat < FILENAME.smt2