===============================================================================

                                OptiMathSAT

                    http://optimathsat.disi.unitn.it/

===============================================================================

OptiMathSAT is a state-of-the-art Optimization Modulo Theories (OMT) solver
based on the SMT solver MathSAT5 (http://mathsat.fbk.eu/). OptiMathSAT features
both single- and multi-objective optimization over arbitrary sets of Linear
Rational Arithmetic (LRA), Linear Integer Arithmetic (LIA), Linear Integer and
Rational Arithmetic (LIRA), Bit-Vectors (BV), Floating-Point (FP),
Pseudo-Boolean (PB) and MaxSMT cost functions. Multiple objective functions
can be combined with one another into a Lexicographic or a Pareto optimization
problem, or independently solved in a single run (for the best efficiency).

Satisfiability Modulo Theories (SMT) is the problem of deciding the
satisfiability of a first-order formula with respect to a combination of
decidable first-order theories. Typical theories of SMT interest are (the
theory of) linear arithmetic over the rationals (LRA), the integers (LIA)
or their combination (LIRA), non-linear arithmetic over the rationals (NLRA)
or the integers (NLIA), arrays (AR), bit-vectors (BV), floating-point
arithmetic (FP), and their combination thereof. The last two decades have
witnessed the development of very efficient SMT solvers based on the so-called
lazy-SMT schema. 

Optimization Modulo Theories (OMT) is an extension to Satisfiability Modulo
Theories (SMT) that allows for finding a model of a first-order formula that
is optimal with respect to some objective function expressed in some background
theory, by means of a combination of SMT and optimization procedures. 



Distinctive Features:

1. Multi-Objective optimization


    OptiMathSAT extends the FlatZinc with Multi-Objective optimization, e.g.

        solve minimize cost, maximize revenue;

    Multiple objectives are combined together using the strategy specified by
    the option '-opt.priority=[box|lex|par]', that is:

    - par: performs a classic Pareto-front exploration
    - lex: optimizes the objectives in lexicographic order
    - box: optimizes each objective independently from the others

2. Infinite-Precision Arithmetic: every arithmetical operation is performed
   with an infinite precision arithmetic library (e.g. GMP) to ensure the
   correctness of the result with absolute precision. Unbounded variables are
   assumed to have an infinite domain ]-INF, +INF[.


3. OptiMathSAT can be used as a FZN2OMT interface to other OMT solvers like
   Z3 (https://github.com/Z3Prover/z3) and Barcelogic (https://barcelogic.com/).
   To discover more about this, see https://github.com/PatrickTrentin88/fzn2omt .



The OptiMathSAT team is comprised by:

    - Roberto Sebastiani, founder, from 2009 to present
      (Associate Professor at University of Trento - DISI, Italy)
    - Silvia Tomasi, founder, from 2009 to 2014
      (Former PhD Student, University of Trento - DISI, Italy)
    - Patrick Trentin, from June 2013 to June 2020
      (Former PhD Student/Post-Doc, University of Trento - DISI, Italy)



Publications:

    [cpaior_cts20]
        F. Contaldo, P. Trentin and R. Sebastiani.
        From MiniZinc to Optimization Modulo Theories, and Back.
        CPAIOR 2020 (To Appear)

    [cade_st19]
        P. Trentin and R. Sebastiani.
        Optimization Modulo the Theory of Floating-Point Numbers.
        Automated Deduction, CADE 27, 2019.
        (https://doi.org/10.1007/978-3-030-29436-6_33)

    [st_jar18]
        R. Sebastiani and P. Trentin.
        OptiMathSAT: A Tool for Optimization Modulo Theories.
        Journal of Automated Reasoning, December 2018.
        (https://doi.org/10.1007/s10817-018-09508-6)

    [st_tacas17]
        R. Sebastiani and P. Trentin.
        On Optimization Modulo Theories, MaxSMT and Sorting Networks.
        In Proc. Int. Converence on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017.

    [st_cav15]
        R. Sebastiani and P. Trentin.
        OptiMathSAT: A Tool for Optimization Modulo Theories.
        In Proc. International Converence on Computer-Aided Verification, CAV 2015.

    [st_tacas15]
        R. Sebastiani and P. Trentin.
        Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions.
        TACAS, 2015.

    [st_tocl14] R. Sebastiani and S. Tomasi.
        Optimization Modulo Theories with Linear Rational Costs.
        ACM Transactions on Computational Logic, March 2015.

    [st-ijcar12]
        R. Sebastiani and S. Tomasi.
        Optimization in SMT with LA(Q) Cost Functions.
        IJCAR, July 2012.
        (http://dx.doi.org/10.1007/978-3-642-31365-3_38)