Advertisement

Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions

  • R. Sebastiani
  • P. Trentin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)

Abstract

In the last decade we have witnessed an impressive progress in the expressiveness and efficiency of Satisfiability Modulo Theories (SMT) solving techniques. This has brought previously-intractable problems at the reach of state-of-the-art SMT solvers, in particular in the domain of SW and HW verification. Many SMT-encodable problems of interest, however, require also the capability of finding models that are optimal wrt. some cost functions. In previous work, namely Optimization Modulo Theory with Linear Rational Cost Functions – OMT( \(\mathcal{LRA}\cup \mathcal{T}\)), we have leveraged SMT solving to handle the minimization of cost functions on linear arithmetic over the rationals, by means of a combination of SMT and LP minimization techniques.

In this paper we push the envelope of our OMT approach along three directions: first, we extend it to work with linear arithmetic on the mixed integer/rational domain, by means of a combination of SMT, LP and ILP minimization techniques; second, we develop a multi-objective version of OMT, so that to handle many cost functions simultaneously or lexicographically; third, we develop an incremental version of OMT, so that to exploit the incrementality of some OMT-encodable problems. An empirical evaluation performed on OMT-encoded verification problems demonstrates the usefulness and efficiency of these extensions.

Keywords

Cost Function Truth Assignment Unit Clause Bound Model Check Incremental Version 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying Industrial Hybrid Systems with MathSAT. In: Proc. BMC 2004. ENTCS, vol. 119. Elsevier (2005)Google Scholar
  2. 2.
    Audemard, G., Cimatti, A., Korniłowicz, A., Sebastiani, R.: SAT-Based Bounded Model Checking for Timed Systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, Springer, Heidelberg (2002)Google Scholar
  3. 3.
    Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Biere et al. [4], ch. 26, vol. 185, pp. 825–885 (February 2009)Google Scholar
  4. 4.
    Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press (February 2009)Google Scholar
  5. 5.
    Bjorner, N., Phan, A.-D.: νZ - Maximal Satisfaction with Z3. In: Proc. SCSS Invited Presentation, Gammart, Tunisia. EasyChair Proceedings in Computing, EPiC (December 2014), http://www.easychair.org/publications/?page=862275542
  6. 6.
    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), 1493–1525 (2006)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Byrd, R.H., Goldman, A.J., Heller, M.: Technical Note– Recognizing Unbounded Integer Programs. Operations Research 35(1) (1987)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A Modular Approach to MaxSAT Modulo Theories. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 150–165. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  10. 10.
    Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)Google Scholar
  11. 11.
    Dillig, I., Dillig, T., McMillan, K.L., Aiken, A.: Minimum Satisfying Assignments for SMT. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 394–409. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Griggio, A.: A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. Journal on Satisfiability, Boolean Modeling and Computation - JSAT 8, 1–27 (2012)MathSciNetGoogle Scholar
  15. 15.
    Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 333–350. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  16. 16.
    Li, Y., Albarghouthi, A., Kincad, Z., Gurfinkel, A., Chechik, M.: Symbolic Optimization with SMT Solvers. In: POPL. ACM Press (2014)Google Scholar
  17. 17.
    Manolios, P., Papavasileiou, V.: ILP modulo theories. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 662–677. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM 53(6), 937–977 (2006)CrossRefMathSciNetGoogle Scholar
  20. 20.
    Sebastiani, R.: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, JSAT 3(3-4), 141–224 (2007)zbMATHMathSciNetGoogle Scholar
  21. 21.
    Sebastiani, R., Tomasi, S.: Optimization Modulo Theories with Linear Rational Costs. To Appear on ACM Transactions on Computational Logics, TOCL, http://optimathsat.disi.unitn.it/pages/publications.html
  22. 22.
    Sebastiani, R., Tomasi, S.: Optimization in SMT with LA(Q) Cost Functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 484–498. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • R. Sebastiani
    • 1
  • P. Trentin
    • 1
  1. 1.DISIUniversity of TrentoTrentoItaly

Personalised recommendations