Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories | SpringerLink
Skip to main content
Springer Nature Link
Log in

Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

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

Included in the following conference series:

Abstract

Solving optimization problems with SAT has a long tradition in the form of MaxSAT, which maximizes the weight of satisfied clauses in a propositional formula. The extension to maximum satisfiability modulo theories (MaxSMT) is less mature but allows problems to be formulated in a higher-level language closer to actual applications. In this paper we describe a new approach for solving MaxSMT based on lifting one of the currently most successful approaches for MaxSAT, the implicit hitting set approach, from the propositional level to SMT. We also provide a unifying view of how optimization, propositional reasoning, and theory reasoning can be combined in a MaxSMT solver. This leads to a generic framework that can be instantiated in different ways, subsuming existing work and supporting new approaches. Experiments with two instantiations clearly show the benefit of our generic framework.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    IHS MaxSAT solvers can be obtained by using the A-Sat rules and replacing \( T\text{- }SAT (AM,F)\) in ImprovedSolution with \( SAT (AM,F)\).

References

  1. Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL, pp. 607–618. ACM (2014)

    Google Scholar 

  2. 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). https://doi.org/10.1007/11814948_18

    Chapter  MATH  Google Scholar 

  3. 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). https://doi.org/10.1007/978-3-642-39071-5_12

    Chapter  Google Scholar 

  4. Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Log. 16(2), 12:1–12:43 (2015)

    Article  MathSciNet  Google Scholar 

  5. Bjørner, N., Phan, A.-D., Fleckenstein, L.: vZ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_14

    Chapter  Google Scholar 

  6. Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 447–454. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_27

    Chapter  Google Scholar 

  7. Manolios, P., Pais, J., Papavasileiou, V.: The Inez mathematical programming modulo theories framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 53–69. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_4

    Chapter  Google Scholar 

  8. Sebastiani, R., Trentin, P.: On optimization modulo theories, MaxSMT and sorting networks. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 231–248. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_14

    Chapter  Google Scholar 

  9. Ansótegui, C., Bacchus, F., Järvisalo, M., Martins, R.: MaxSAT evaluation 2017 (2017). http://mse17.cs.helsinki.fi/

  10. Bacchus, F., Järvisalo, M.: Algorithms for maximum satisfiability with applications to AI. In: AAAI-2016 Tutoral (2016). https://www.cs.helsinki.fi/group/coreo/aaai16-tutorial/

  11. Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225–239. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23786-7_19

    Chapter  Google Scholar 

  12. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Lovel and procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)

    Article  MathSciNet  Google Scholar 

  13. Sebastiani, R.: Lazy satisability modulo theories. JSAT 3(3–4), 141–224 (2007)

    MathSciNet  MATH  Google Scholar 

  14. Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI, pp. 2717–2723. AAAI Press (2014)

    Google Scholar 

  15. Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531–548. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10428-7_39

    Chapter  Google Scholar 

  16. Ansótegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77–105 (2013)

    Article  MathSciNet  Google Scholar 

  17. 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). https://doi.org/10.1007/978-3-540-24605-3_37

    Chapter  Google Scholar 

  18. Chandrasekaran, K., Karp, R.M., Moreno-Centeno, E., Vempala, S.: Algorithms for implicit hitting set problems. In: SODA, SIAM, pp. 614–629 (2011)

    Chapter  Google Scholar 

  19. Saikko, P., Wallner, J.P., Järvisalo, M.: Implicit hitting set algorithms for reasoning beyond NP. In: KR, pp. 104–113. AAAI Press (2016)

    Google Scholar 

  20. Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247–262. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40627-0_21

    Chapter  Google Scholar 

  21. Lagniez, J.-M., Biere, A.: Factoring out assumptions to speed Up MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 276–292. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_21

    Chapter  Google Scholar 

  22. Ansótegui, C., Gabàs, J., Levy, J.: Exploiting subproblem optimization in SAT-based MaxSAT algorithms. J. Heuristics 22(1), 1–53 (2016)

    Article  Google Scholar 

  23. 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). https://doi.org/10.1007/978-3-642-36742-7_7

    Chapter  MATH  Google Scholar 

  24. Bofill, M., Muñoz, V., Murillo, J.: Solving the wastewater treatment plant problem with SMT. CoRR abs/1609.05367 (2016)

    Google Scholar 

  25. Marques-Silva, J., Argelich, J., Graça, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. AI 62(3–4), 317–343 (2011)

    MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

This research has been supported by the Austrian Science Fund (FWF) under projects W1255-N23 and S11408-N23.

Author information

Authors and Affiliations

  1. Johannes Kepler University, Linz, Austria

    Katalin Fazekas & Armin Biere

  2. University of Toronto, Toronto, Canada

    Fahiem Bacchus

Authors
  1. Katalin Fazekas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fahiem Bacchus
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Armin Biere
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Katalin Fazekas .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Fazekas, K., Bacchus, F., Biere, A. (2018). Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation