Skip to main content
SpringerLink
Log in

Satisfiability Modulo Theories and Assignments

  • Conference paper
  • First Online:
Automated Deduction – CADE 26 (CADE 2017)

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

Included in the following conference series:

Abstract

The CDCL procedure for SAT is the archetype of conflict-driven procedures for satisfiability of quantifier-free problems in a single theory. In this paper we lift CDCL to CDSAT (Conflict-Driven Satisfiability), a system for conflict-driven reasoning in combinations of disjoint theories. CDSAT combines theory modules that interact through a global trail representing a candidate model by Boolean and first-order assignments. CDSAT generalizes to generic theory combinations the model-constructing satisfiability calculus (MCSAT) introduced by de Moura and Jovanović. Furthermore, CDSAT generalizes the equality sharing (Nelson-Oppen) approach to theory combination, by allowing theories to share equality information both explicitly through equalities and disequalities, and implicitly through assignments. We identify sufficient conditions for the soundness, completeness, and termination of CDSAT.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

References

  1. Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512–526. Springer, Heidelberg (2006). doi:10.1007/11916277_35

    Chapter  Google Scholar 

  2. Bonacina, M.P.: On conflict-driven reasoning. In: Dutertre, B., Shankar, N. (eds.) Proceedings of the Sixth Workshop on Automated Formal Methods (AFM), at the Ninth NASA Formal Methods Symposium (NFM), pp. 1–9 (2017, to appear). http://fm.csl.sri.com/AFM17/

  3. Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: A model-constructing framework for theory combination. Technical Report 99/2016, Dipartimento di Informatica, Università degli Studi di Verona, Verona, Italy, EU. https://hal.archives-ouvertes.fr/hal-01425305, also Technical report of SRI International and INRIA - CNRS - École Polytechnique; Revised April 2017

  4. Cotton, S.: Natural domain SMT: a preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 77–91. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15297-9_8

    Chapter  Google Scholar 

  5. Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35873-9_1

    Chapter  Google Scholar 

  6. Ganzinger, H., Rueß, H., Shankar, N.: Modularity and refinement in inference systems. Technical report CSL-SRI-04-02, Computer Science Laboratory, SRI International, Menlo Park, CA, USA (2004)

    Google Scholar 

  7. Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Cabodi, G., Singh, S. (eds.) Proceedings of the Twelfth International Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE (2012)

    Google Scholar 

  8. Jovanović, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330–346. Springer, Heidelberg (2017). doi:10.1007/978-3-319-52234-0_18

    Chapter  Google Scholar 

  9. Jovanović, D., Barrett, C., de Moura, L.: The design and implementation of the model-constructing satisfiability calculus. In: Jobstman, B., Ray, S. (eds.) Proceedings of the Thirteenth Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE (2013)

    Google Scholar 

  10. Jovanović, D., Moura, L.: Cutting to the chase: solving linear integer arithmetic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 338–353. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_26

    Chapter  Google Scholar 

  11. Jovanović, D., Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31365-3_27

    Chapter  Google Scholar 

  12. Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 509–523. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04244-7_41

    Chapter  Google Scholar 

  13. Krstić, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS (LNAI), vol. 4720, pp. 1–27. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74621-8_1

    Chapter  Google Scholar 

  14. Marques Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131–153. IOS Press (2009)

    Google Scholar 

  15. McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer Logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462–476. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_35

    Chapter  Google Scholar 

  16. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Prog. Lang. Syst. 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  17. Wang, C., Ivančić, F., Ganai, M., Gupta, A.: Deciding separation logic formulae by SAT and incremental negative cycle elimination. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 322–336. Springer, Heidelberg (2005). doi:10.1007/11591191_23

    Chapter  Google Scholar 

  18. Wolfman, S.A., Weld, D.S.: The LPSAT engine and its application to resource planning. In: Dean, T. (ed.) Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI), vol. 1, pp. 310–316. Morgan Kaufmann Publishers (1999)

    Google Scholar 

  19. Zeljić, A., Wintersteiger, C.M., Rümmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 249–266. Springer, Heidelberg (2016). doi:10.1007/978-3-319-40970-2_16

    Google Scholar 

Download references

Acknowledgments

The authors thank Dejan Jovanović for fruitful discussions. Part of this research was conducted while the first author was an international fellow at the Computer Science Laboratory of SRI International, whose support is greatly appreciated. This research was funded in part by NSF grants 1528153 and CNS-0917375, by DARPA under agreement number FA8750-16-C-0043, and by grant “Ricerca di base 2015” of the Università degli Studi di Verona. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of NSF, DARPA, or the U.S. Government.

Author information

Authors and Affiliations

  1. Università degli Studi di Verona, Verona, Italy

    Maria Paola Bonacina

  2. SRI International, Menlo Park, USA

    Stéphane Graham-Lengrand & Natarajan Shankar

  3. CNRS - INRIA - École Polytechnique, Palaiseau, France

    Stéphane Graham-Lengrand

Authors
  1. Maria Paola Bonacina
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stéphane Graham-Lengrand
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Natarajan Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maria Paola Bonacina .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Leonardo de Moura

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bonacina, M.P., Graham-Lengrand, S., Shankar, N. (2017). Satisfiability Modulo Theories and Assignments. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63046-5_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63045-8

  • Online ISBN: 978-3-319-63046-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation