Skip to main content
SpringerLink
Log in

Optimization in SMT with \({\mathcal LA}\)(ℚ) Cost Functions

  • Conference paper
Book cover Automated Reasoning (IJCAR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 7364))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. http://disi.unitn.it/~rseba/ijcar12/ijcar12-tarball.tar.gz

  2. EMP, http://www.gams.com/dd/docs/solvers/emp.pdf

  3. JAMS, http://www.gams.com/

  4. LogMIP v2.0, http://www.logmip.ceride.gov.ar/index.html

  5. MathSAT 5, http://mathsat.fbk.eu/

  6. SMT-LIB, http://www.smtlib.org/

  7. Yices, http://yices.csl.sri.com/

  8. 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)

    Chapter  Google Scholar 

  9. 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)

    Google Scholar 

  10. Balas, E.: Disjunctive programming: Properties of the convex hull of feasible points. Discrete Applied Mathematics 89(1-3), 3–44 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  11. Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Biere et al [12], ch. 26, pp. 825–885 (February 2009)

    Google Scholar 

  12. 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)

    Google Scholar 

  13. 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)

    Google Scholar 

  14. Brooke, A., Kendrick, D., Meeraus, A., Raman, R.: GAMS - A User’s Guide. In: GAMS Development Corporation, Washington, DC, USA (2011)

    Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Griggio, A.: A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. Journal on Satisfiability, Boolean Modeling and Computation - JSAT 8, 1–27 (2012)

    Google Scholar 

  18. IBM. IBM ILOG CPLEX Optimizer (2010), http://www-01.ibm.com/software/integration/optimization/cplex-optimizer/

  19. Li, C.M., Manyà, F.: MaxSAT, Hard and Soft Constraints. In: Biere et al. [12], ch.19, pp. 613–631 (February 2009)

    Google Scholar 

  20. Lodi, A.: Mixed Integer Programming Computation. In: 50 Years of Integer Programming 1958-2008, pp. 619–645. Springer (2009)

    Google Scholar 

  21. Lynce, I., Marques-Silva, J.: On Computing Minimum Unsatisfiable Cores. In: SAT (2004)

    Google Scholar 

  22. 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)

    Google Scholar 

  23. Nelson, C.G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  24. 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)

    Chapter  Google Scholar 

  25. Raman, R., Grossmann, I.: Modelling and computational techniques for logic based integer programming. Computers and Chemical Engineering 18(7), 563–578 (1994)

    Article  Google Scholar 

  26. Roussel, O., Manquinho, V.: Pseudo-Boolean and Cardinality Constraints. In: Biere et al [12], ch. 22, pp. 695–733 (February 2009)

    Google Scholar 

  27. 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)

    Article  Google Scholar 

  28. 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)

    Article  MathSciNet  MATH  Google Scholar 

  29. 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

  30. 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)

    Chapter  Google Scholar 

  31. Vecchietti, A.: Personal communication (2011)

    Google Scholar 

  32. Vecchietti, A., Grossmann, I.: Computational experience with logmip solving linear and nonlinear disjunctive programming problems. In: Proc. of FOCAPD, pp. 587–590 (2004)

    Google Scholar 

  33. Wolfman, S., Weld, D.: The LPSAT Engine & its Application to Resource Planning. In: Proc. IJCAI (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISI, University of Trento, Italy

    Roberto Sebastiani & Silvia Tomasi

Authors
  1. Roberto Sebastiani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvia Tomasi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9, E185/2, 1040, Wien, Austria

    Bernhard Gramlich

  2. École Polytechnique, INRIA Saclay and Laboratoire d’Informatique, Route de Saclay, 91128, Palaiseau Cedex, France

    Dale Miller

  3. School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Uli Sattler

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation