×

OptiMathSAT: a tool for optimization modulo theories. (English) Zbl 1468.68206

Summary: Optimization Modulo Theories \(( \text{OMT})\) is an extension of SMT which allows for finding models that optimize given objectives. OptiMathSAT is an OMT solver which allows for solving a list of optimization problems on SMT formulas with linear objective functions – on the Boolean, the rational and the integer domains, and on their combination thereof – including (partial weighted) MaxSMT. Multiple and heterogeneous objective functions can be combined together and handled either independently, or lexicographically, or in linear or min-max/max-min combinations. OptiMathSAT provides an incremental interface, it supports both an extended version of the SMT-LIBv2 language and a subset of the FlatZinc language, and can be interfaced via an API. In this paper we describe OptiMathSAT and its usage in full detail.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
90C29 Multi-objective and goal programming
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] CGM-Tool. http://www.cgm-tool.eu
[2] D-wave 2x tecnology overview. https://www.dwavesys.com/sites/default/files/D-Wave
[3] Experimental data. http://disi.unitn.it/trentin/resources/jar2017.tar.gz
[4] FlatZinc 1.6. http://www.minizinc.org/downloads/doc-1.6/flatzinc-spec.pdf
[5] LMT. http://disi.unitn.it/ teso/lmt/lmt.tgz
[6] MiniZinc 1.6. http://www.minizinc.org/downloads/doc-1.6/zinc-spec.pdf
[7] OptiMathSAT. http://optimathsat.disi.unitn.it
[8] PyLMT. http://www.bitbucket.org/stefanoteso/pylmt
[9] FlatZinc support in OptiMathSAT. http://optimathsat.disi.unitn.it/pages/fznreference.html
[10] WCET OMT. https://github.com/PatrickTrentin88/wcet_omt
[11] Abío, Ignasi; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric, A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints, Lecture Notes in Computer Science, 80-96 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[12] Achterberg, T., Scip: solving constraint integer programs, Math. Program. Comput., 1, 1, 1-41 (2009) · Zbl 1171.90476
[13] Achterberg, T., Berthold, T., Koch, T., Wolter, K.: Constraint integer programming: a new approach to integrate CP and MIP. In: Proceedings of CPAIOR’08, LNCS, pp. 6-20. Springer (2008) · Zbl 1142.68504
[14] Ansótegui, C., Bofill, M., Palahí, M., Suy, J., Villaret, M.: Satisfiability modulo theories: an efficient approach for the resource-constrained project scheduling problem. In: SARA (2011) · Zbl 1309.90083
[15] Balas, E., Disjunctive programming: properties of the convex hull of feasible points, Discrete Appl. Math., 89, 1-3, 3-44 (1998) · Zbl 0921.90118
[16] Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The satisfiability modulo theories library (smt-lib) (2010). http://www.smtlib.org
[17] Barrett, C.; Sebastiani, R.; Seshia, Sa; Tinelli, C.; Biere, A., Satisfiability modulo theories, chapter 26, Handbook of Satisfiability, 825-885 (2009), Amsterdam: IOS Press, Amsterdam
[18] Bian, Z.; Chudak, F.; Israel, R.; Lackey, B.; Macready, Wg; Roy, A., Discrete optimization using quantum annealing on sparse Ising models, Front. Phys., 2, 56 (2014)
[19] Bian, Z.; Chudak, F.; Macready, W.; Roy, A.; Sebastiani, R.; Varotti, S.; Dixon, C.; Finger, M., Solving SAT and MaxSAT with a quantum annealer: foundations and a preliminary report, Frontiers of Combining Systems, LNCS, 153-171 (2017), Berlin: Springer, Berlin · Zbl 06821632
[20] Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009) · Zbl 1183.68568
[21] Bjorner, N.: Personal communication, 02 (2016)
[22] Bjorner, N., Phan, A.-D.: \( \nu{}Z\)—Maximal satisfaction with Z3. In: Proceedings of International Symposium on Symbolic Computation in Software Science, Gammart, Tunisia, December 2014. EasyChair Proceedings in Computing (EPiC). http://www.easychair.org/publications/?page=862275542
[23] Bjorner, N., Phan, A.-D., Fleckenstein, L.: Z3—an optimizing SMT solver. In: Proceedings of TACAS, LNCS, vol. 9035. Springer, Berlin (2015)
[24] Bofill, M., Palahı, M., Suy, J., Villaret, M.: Simply: a compiler from a csp modeling language to the smt-lib format. In: Proceedings of the 8th International Workshop on Constraint Modelling and Reformulation, pp. 30-44 (2009)
[25] Bofill, M.; Palahí, M.; Suy, J.; Villaret, M., Solving constraint satisfaction problems with SAT modulo theories, Constraints, 17, 3, 273-303 (2012) · Zbl 1309.90099
[26] Bofill, M., Palahı, M., Villaret, M.: A system for CSP solving through satisfiability modulo theories. IX Jornadas sobre Programación y Lenguajes (PROLE09), pp. 303-312 (2009)
[27] Bofill, Miquel; Suy, Josep; Villaret, Mateu, A System for Solving Constraint Satisfaction Problems with SMT, Theory and Applications of Satisfiability Testing - SAT 2010, 300-305 (2010), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1306.68153
[28] Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, Ta; Ranise, S.; Van Rossum, P.; Sebastiani, R., Efficient theory combination via Boolean search, Inf. Comput., 204, 10, 1493-1525 (2006) · Zbl 1137.68578
[29] Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel, Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL, Static Analysis, 412-432 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1426.68249
[30] Brain, M.; D’Silva, V.; Griggio, A.; Haller, L.; Kroening, D., Deciding floating-point logic with abstract conflict driven clause learning, Form. Methods Syst. Des., 45, 2, 213-245 (2014) · Zbl 1317.68110
[31] Byrd, Rh; Goldman, Aj; Heller, M., Technical note-recognizing unbounded integer programs, Oper. Res., 35, 1, 140-142 (1987) · Zbl 0614.90080
[32] Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: Foundations and applications. In: TACAS, LNCS, vol. 6015, pp. 99-113. Springer, Berlin (2010) · Zbl 1284.68388
[33] Cimatti, A.; Griggio, A.; Irfan, A.; Roveri, M.; Sebastiani, R., Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF, 58-75 (2017), Berlin: Springer, Berlin
[34] Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto, Satisfiability Modulo Transcendental Functions via Incremental Linearization, Automated Deduction - CADE 26, 95-113 (2017), Cham: Springer International Publishing, Cham · Zbl 06778399
[35] Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto, A Modular Approach to MaxSAT Modulo Theories, Theory and Applications of Satisfiability Testing - SAT 2013, 150-165 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1390.68572
[36] Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto, The MathSAT5 SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, 93-107 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1381.68153
[37] Cimatti, A.; Griggio, A.; Sebastiani, R., Efficient generation of craig interpolants in satisfiability modulo theories, ACM Trans. Comput. Logics TOCL, 12, 1, 7 (2010) · Zbl 1351.68247
[38] Cimatti, A.; Griggio, A.; Sebastiani, R., Computing small unsatisfiable cores in SAT modulo theories, J. Artif. Intell. Res. JAIR, 40, 701-728 (2011) · Zbl 1216.68241
[39] Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: CAV, LNCS, vol. 4144 (2006)
[40] Dutertre, B., de Moura, L.: System description: Yices 1.0. In: Proceedings on 2nd SMT competition, SMT-COMP’06 (2006). https://www.yices.csl.sri.com/papers/yices-smtcomp06.pdf
[41] Eén, Niklas; Sörensson, Niklas, An Extensible SAT-solver, Theory and Applications of Satisfiability Testing, 502-518 (2004), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1204.68191
[42] Feydy, Thibaut; Stuckey, Peter J., Lazy Clause Generation Reengineered, Principles and Practice of Constraint Programming - CP 2009, 352-366 (2009), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[43] Griggio, A., A practical approach to satisfiability modulo linear integer arithmetic, J. Satisf. Boolean Model. Comput. JSAT, 8, 1-27 (2012) · Zbl 1331.68207
[44] Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Proceedings of FMCAD (2012) (to appear) · Zbl 1317.68110
[45] Henry, J.; Asavoae, M.; Monniaux, D.; Maïza, C., How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics, SIGPLAN Not., 49, 5, 43-52, 06 (2014)
[46] Johnson, Mw; Amin, Mhs; Gildert, S.; Lanting, T.; Hamze, F.; Dickson, N.; Harris, R.; Berkley, Aj; Johansson, J.; Bunyk, P.; Chapple, Em; Enderud, C.; Hilton, Jp; Karimi, K.; Ladizinsky, E.; Ladizinsky, N.; Oh, T.; Perminov, I.; Rich, C.; Thom, Mc; Tolkacheva, E.; Truncik, Cjs; Uchaikin, S.; Wang, J.; Wilson, B.; Rose, G., Quantum annealing with manufactured spins, Nature, 473, 7346, 194-198 (2011)
[47] Lahiri, Shuvendu K.; Nieuwenhuis, Robert; Oliveras, Albert, SMT Techniques for Fast Predicate Abstraction, Computer Aided Verification, 424-437 (2006), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[48] Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: SAT (2014) · Zbl 1423.68457
[49] Laumanns, M., Thiele, L., Zitzler, E.: An adaptive scheme to generate the pareto front based on the epsilon-constraint method. In: Branke, J., Deb, K., Miettinen, K., Steuer, R.E.: (eds.), Practical Approaches to Multi-Objective Optimization, number 04461 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, (2005). Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany
[50] Legriel, J.; Le Guernic, C.; Cotton, S.; Maler, O.; Esparza, J.; Majumdar, R., Approximating the pareto front of multi-criteria optimization problems, Tools and Algorithms for the Construction and Analysis of Systems, LNCS, 69-83 (2010), Berlin: Springer, Berlin · Zbl 1284.90074
[51] Li, Y., Albarghouthi, A., Kincad, Z., Gurfinkel, A., Chechik, M.: Symbolic Optimization with SMT Solvers. In: POPL (2014) · Zbl 1284.68410
[52] Lodi, A.; Jünger, M., Mixed integer programming computation, 50 Years of Integer Programming 1958-2008, 619-645 (2009), Berlin: Springer, Berlin · Zbl 1187.90206
[53] Manolios, Panagiotis; Papavasileiou, Vasilis, ILP Modulo Theories, Computer Aided Verification, 662-677 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[54] Marques-Silva, J.; Argelich, J.; Graa, A.; Lynce, I., Boolean lexicographic optimization: algorithms applications, Ann. Math. Artif. Intell., 62, 3-4, 317-343 (2011) · Zbl 1242.90199
[55] Marques-Silva, Jp; Lynce, I.; Malik, S.; Biere, M., Conflict-driven clause learning SAT solvers, chapter 4, Handbook of Satisfiability, 131-153 (2009), Berlin: Springer, Berlin
[56] MiniZinc. www.minizinc.org
[57] Nadel, A.; Ryvchin, V.; Chechik, M.; Raskin, Jf, Bit-vector optimization, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2016, LNCS (2016), Berlin: Springer, Berlin
[58] Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided maxsat resolution. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27-31, 2014, Québec City, Québec, Canada, pp. 2717-2723. AAAI Press (2014)
[59] Nguyen, Chi Mai; Sebastiani, Roberto; Giorgini, Paolo; Mylopoulos, John, Multi-objective reasoning with constrained goal models, Requirements Engineering, 23, 2, 189-225 (2016)
[60] Nguyen, C.M., Sebastiani, R., Giorgini, P., Mylopoulos, J.: Requirements evolution and evolution requirements with constrained goal models. In: Proceedings of the 37nd International Conference on Conceptual Modeling-ER16, LNCS. Springer (2016)
[61] Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Proceedings of Theory and Applications of Satisfiability Testing-SAT 2006, LNCS, vol. 4121. Springer (2006) · Zbl 1187.68558
[62] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), J. ACM, 53, 6, 937-977 (2006) · Zbl 1326.68164
[63] Ohrimenko, O.; Stuckey, Pj; Codish, M., Propagation = Lazy Clause Generation, 544-558 (2007), Berlin: Springer, Berlin · Zbl 1145.68527
[64] Ohrimenko, O.; Stuckey, Pj; Codish, M., Propagation via lazy clause generation, Constraints, 14, 3, 357-391 (2009) · Zbl 1192.68654
[65] Raman, R.; Grossmann, I., Modelling and computational techniques for logic based integer programming, Comput. Chem. Eng., 18, 7, 563-578 (1994)
[66] Rayside, D., Estler, H.-C., Jackson, D.: The guided improvement algorithm for exact, general-purpose, many-objective combinatorial optimization. Technical Report, Massachusetts Institute of Technology, Cambridge, 07 (2009)
[67] Sawaya, Nw; Grossmann, Ie, A cutting plane method for solving linear generalized disjunctive programming problems, Comput. Chem. Eng., 29, 9, 1891-1913 (2005)
[68] Sawaya, Nw; Grossmann, Ie, A hierarchy of relaxations for linear generalized disjunctive programming, Eur. J. Oper. Res., 216, 1, 70-82 (2012) · Zbl 1266.90132
[69] Sebastiani, R., Lazy satisfiability modulo theories, J. Satisf. Boolean Model. Comput. JSAT, 3, 3-4, 141-224 (2007) · Zbl 1145.68501
[70] Sebastiani, R., Tomasi, S.: Optimization in SMT with LA(Q) cost functions. In: IJCAR, LNAI, vol. 7364, pp. 484-498. Springer (2012) · Zbl 1358.68264
[71] Sebastiani, R.; Tomasi, S., Optimization modulo theories with linear rational costs, ACM Trans. Comput. Logics, 16, 2, 12 (2015) · Zbl 1354.68233
[72] Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Proceedings of International Conference on Computer-Aided Verification, CAV 2015, LNCS, vol. 9206. Springer (2015) · Zbl 1420.68197
[73] Sebastiani, R., Trentin, P.: Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’15, LNCS, vol. 9035. Springer (2015) · Zbl 1420.68197
[74] Sebastiani, R., Trentin, P.: On optimization modulo theories, maxsmt and sorting networks. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’17, LNCS, vol. 10205. Springer (2017)
[75] Sinz, C.; Van Beek, P., Towards an optimal CNF encoding of Boolean cardinality constraints, Principles and Practice of Constraint Programming, CP, LNCS, 827-831 (2005), Berlin: Springer, Berlin · Zbl 1153.68488
[76] Teso, S.; Sebastiani, R.; Passerini, A., Structured learning modulo theories, Artif. Intell., 244, 166-187 (2017) · Zbl 1404.68121
[77] Van Lamsweerde, A.: Goal-oriented requirements engineering: a guided tour. In: Proceedings of the Fifth IEEE International Conference on Requirements Engineering, RE’01, pp. 249. IEEE Computer Society (2001)
[78] Vecchietti, A., Grossmann, I.: Computational experience with logmip solving linear and nonlinear disjunctive programming problems. In: Proceedings of FOCAPD, pp. 587-590 (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.