Abstract
In the contexts of automated reasoning and formal verification, important decision problems are effectively encoded into Satisfiability Modulo Theories (SMT). In the last decade efficient SMT solvers have been developed for several theories of practical interest (e.g., linear arithmetic, arrays, bit-vectors). Surprisingly, very little work has been done to extend SMT to deal with optimization problems; in particular, we are not aware of any work on SMT solvers able to produce solutions which minimize cost functions over arithmetical variables. This is unfortunate, since some problems of interest require this functionality.
In this paper we start filling this gap. We present and discuss two general procedures for leveraging SMT to handle the minimization of \({\mathcal LA}\)(ℚ) cost functions, combining SMT with standard minimization techniques. We have implemented the procedures within the MathSAT SMT solver. Due to the absence of competitors in AR and SMT domains, we have experimentally evaluated our implementation against state-of-the-art tools for the domain of linear generalized disjunctive programming (LGDP), which is closest in spirit to our domain, on sets of problems which have been previously proposed as benchmarks for the latter tools. The results show that our tool is very competitive with, and often outperforms, these tools on these problems, clearly demonstrating the potential of the approach.
R. Sebastiani is supported by Semiconductor Research Corporation under GRC Custom Research Project 2009-TJ-1880 WOLFLING and GRC Research Project 2012-TJ-2266 WOLF.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
JAMS, http://www.gams.com/
LogMIP v2.0, http://www.logmip.ceride.gov.ar/index.html
MathSAT 5, http://mathsat.fbk.eu/
SMT-LIB, http://www.smtlib.org/
Yices, http://yices.csl.sri.com/
Achterberg, T., Berthold, T., Koch, T., Wolter, K.: Constraint Integer Programming: A New Approach to Integrate CP and MIP. In: Trick, M.A. (ed.) CPAIOR 2008. LNCS, vol. 5015, pp. 6–20. Springer, Heidelberg (2008)
Audemard, G., Cimatti, A., Korniłowicz, A., Sebastiani, R.: SAT-Based Bounded Model Checking for Timed Systems. In: Proc. FORTE 2002. LNCS, vol. 2529. Springer (2002)
Balas, E.: Disjunctive programming: Properties of the convex hull of feasible points. Discrete Applied Mathematics 89(1-3), 3–44 (1998)
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Biere et al [12], ch. 26, pp. 825–885 (February 2009)
In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (February 2009)
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient Theory Combination via Boolean Search. Information and Computation 204(10) (2006)
Brooke, A., Kendrick, D., Meeraus, A., Raman, R.: GAMS - A User’s Guide. In: GAMS Development Corporation, Washington, DC, USA (2011)
Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability Modulo the Theory of Costs: Foundations and Applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 99–113. Springer, Heidelberg (2010)
Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Griggio, A.: A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. Journal on Satisfiability, Boolean Modeling and Computation - JSAT 8, 1–27 (2012)
IBM. IBM ILOG CPLEX Optimizer (2010), http://www-01.ibm.com/software/integration/optimization/cplex-optimizer/
Li, C.M., Manyà, F.: MaxSAT, Hard and Soft Constraints. In: Biere et al. [12], ch.19, pp. 613–631 (February 2009)
Lodi, A.: Mixed Integer Programming Computation. In: 50 Years of Integer Programming 1958-2008, pp. 619–645. Springer (2009)
Lynce, I., Marques-Silva, J.: On Computing Minimum Unsatisfiable Cores. In: SAT (2004)
Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT Solvers. In: Biere et al [12], ch.4, pp. 131–153 (February 2009)
Nelson, C.G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245–257 (1979)
Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006)
Raman, R., Grossmann, I.: Modelling and computational techniques for logic based integer programming. Computers and Chemical Engineering 18(7), 563–578 (1994)
Roussel, O., Manquinho, V.: Pseudo-Boolean and Cardinality Constraints. In: Biere et al [12], ch. 22, pp. 695–733 (February 2009)
Sawaya, N.W., Grossmann, I.E.: A cutting plane method for solving linear generalized disjunctive programming problems. Comput. Chem. Eng. 29(9), 1891–1913 (2005)
Sawaya, N.W., Grossmann, I.E.: A hierarchy of relaxations for linear generalized disjunctive programming. European Journal of Operational Research 216(1), 70–82 (2012)
Sebastiani, R., Tomasi, S.: Optimization in SMT with LA(Q) Cost Functions. Technical Report DISI-12-003, DISI, University of Trento (January 2012), http://disi.unitn.it/~rseba/ijcar12/DISI-12-003.pdf
Sellmann, M., Kadioglu, S.: Dichotomic Search Protocols for Constrained Optimization. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 251–265. Springer, Heidelberg (2008)
Vecchietti, A.: Personal communication (2011)
Vecchietti, A., Grossmann, I.: Computational experience with logmip solving linear and nonlinear disjunctive programming problems. In: Proc. of FOCAPD, pp. 587–590 (2004)
Wolfman, S., Weld, D.: The LPSAT Engine & its Application to Resource Planning. In: Proc. IJCAI (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sebastiani, R., Tomasi, S. (2012). Optimization in SMT with \({\mathcal LA}\)(ℚ) Cost Functions. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-31365-3_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31364-6
Online ISBN: 978-3-642-31365-3
eBook Packages: Computer ScienceComputer Science (R0)