=============================================================================== 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: 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)