===============================================================================
NOTES
===============================================================================
OptiMathSAT-INT: problems are converted from FlatZinc to in OMT(QF_LIRA), where
QF_LIRA stands for the Theory of Linear Arithmetic, and solved with OptiMathSAT.
OptiMathSAT-INT-SMT2: problems are converted from FlatZinc to in OMT(QF_LIRA),
where QF_LIRA stands for the Theory of Linear Arithmetic, and solved with
OptiMathSAT. This configuration uses custom global constraints for SMT2.
OptiMathSAT-BV: problems are converted from FlatZinc to in OMT(QF_BV), where
QF_BV stands for the Theory of BitVectors, and solved with OptiMathSAT.
Past experimental evidence suggests that QF_LIRA and QF_BV have complementary
advantages and tend to outperform one another on different problems.
Below follows a description of the tools included in this submission.
===============================================================================
fzn2omt
https://github.com/PatrickTrentin88/fzn2omt
===============================================================================
The fzn2omt library is a collection of python scripts to solve FlatZinc models
with Optimization Modulo Theories solvers like, e.g., Barcelogic, OptiMathSAT
and z3.
Satisfaction models can also be solved with Satisfiability Modulo Theory solvers
like, e.g., CVC4.
All tools support the encoding based on the QF_LIRA logic (option --int-enc),
that may sometimes be extended to QF_NIRA when the input problem requires it.
OptiMathSAT, z3 and CVC4 support also the encoding based on the QF_BV logic
(option --bv-enc).
Both OptiMathSAT and z3 support the following multi-objective combinations
over FlatZinc models:
- Multi-Independent optimization (box): each objective is considered an
independent optimization goal from the others, so there is one optimal
solution for each goal;
- Lexicographic optimization (lex): the objectives are optimized in decreasing
order of priority, so there is only one optimal solution;
- Pareto optimization (par): all Pareto-optimal solutions are returned;
A FlatZinc model with multiple objectives may look like:
```
solve minimize cost, maximize profit;
```
To know how to select the desired multi-objective combination with OptiMathSAT
and z3, look at the examples in the official documentation.
Barcelogic does not have native support for multi-objective optimization. Thus,
multiple optimization targets are solved incrementally.
SMT/OMT solvers use infinite-precision arithmetic. Upon user request, models are
printed with finite precision by default. It is possible to print a model with
infinite precision using the option --infinite-precision.
Authors:
Patrick Trentin
(Former PhD Student/Post-Doc, University of Trento - DISI, Italy)
===============================================================================
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)