Top

Journal of Automated Reasoning

Published in:

04-01-2019

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness

Authors: Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar

Published in: Journal of Automated Reasoning | Issue 3/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Many applications depend on solving the satisfiability of formulæ involving propositional logic and first-order theories, a problem known as Satisfiability Modulo Theory. This article presents a new method for satisfiability modulo a combination of theories, named CDSAT, for Conflict-Driven SATisfiability. CDSAT also solves Satisfiability Modulo Assignment problems that may include assignments to first-order terms. A conflict-driven procedure assigns values to variables to build a model, and performs inferences on demand in order to solve conflicts between assignments and formulæ. CDSAT extends this paradigm to generic combinations of disjoint theories, each characterized by a collection of inference rules called theory module. CDSAT coordinates the theory modules in such a way that the conflict-driven reasoning happens in the union of the theories, not only in propositional logic. As there is no fixed hierarchy with propositional logic at the center and the other theories as satellites, CDSAT offers a flexible framework for model search. We prove the soundness, completeness, and termination of CDSAT, identifying sufficient requirements on theories and modules that ensure these properties.

previous article Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

next article SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

In fact, it is an inference system in the sense of [12].

\({\textsf {UndoClear}}\) is a renaming of Undo [5].

\({\textsf {UndoDecide}}\) replaces T-backjump-decide [9] or Semantic split [15].

Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak’s method for combining decision procedures. In: Armando, A. (ed.) Proceedings of the Fourth International Workshop on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 2309, pp. 132–146. Springer, Berlin (2002)

Barrett, C.W., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) Proceedings of the Thirteenth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Lecture Notes in Artificial Intelligence, vol. 4246, pp. 512–526. Springer, Berlin (2006)CrossRef

Bobot, F., Graham-Lengrand, S., Marre, B., Bury, G.: Centralizing equality reasoning in MCSAT. Presented at the Sixteenth International Workshop on Satisfiability Modulo Theories (SMT) at the Ninth International Joint Conference on Automated Reasoning (IJCAR), July (2018)

Bonacina, M.P.: On conflict-driven reasoning. In: Shankar, N., Dutertre, B. (eds.) Proceedings of the Sixth Workshop on Automated Formal Methods (AFM) at the Ninth NASA Formal Methods Symposium (NFM), Kalpa Publications, vol. 5, pp. 31–49. EasyChair (2018)

Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Satisfiability modulo theories and assignments. In: de Moura, L. (ed.) Proceedings of the Twenty-Sixth Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 10395, pp. 42–59. Springer, Berlin (2017)CrossRef

Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Proofs in conflict-driven theory combination. In: Andronick, J., Felty, A. (eds.) Proceedings of the Seventh ACM International Conference on Certified Programs and Proofs (CPP), pp. 186–200. ACM Press, New York (2018)

Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Berlin (2007)MATH

Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. J. Satisf. Boolean Model. Comput. 6, 165–201 (2009)MathSciNetMATH

de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Proceedings of the Fourteenth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 7737, pp. 1–12. Springer, Berlin (2013)

10.

de Moura, L., Passmore, G.O.: Exact global optimization on demand (presentation only). In: Ghilardi, S., Sofronie-Stokkermans, V., Tiwari A. (eds.) Notes of the Third Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT), pp. 50–50 (2013). https://userpages.uni-koblenz.de/~sofronie/addct-2013/. Last seen on 19 Dec. 2018

11.

Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Proceedings of the Twenty-Sixth International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 8559, pp. 737–744. Springer, Berlin, (2014)CrossRef

12.

Ganzinger, H., Rueß, H., Shankar, N.: Modularity and Refinement in Inference Systems. Technical Report CSL-SRI-04-02, CSL, SRI International, Menlo Park, CA, USA (2004)

13.

Jovanović, D: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) Proceedings of the Eighteenth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 10145, pp. 330–346. Springer, Berlin (2017)

14.

Jovanović, D., Barrett, C.W.: Sharing is caring: combination of theories. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Proceedings of the Eighth International Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 6989, pp. 195–210. Springer, Berlin (2011)CrossRef

15.

Jovanović, D., Barrett, C.W., 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)

16.

Jovanović, D., de Moura, L.: Cutting to the chase: solving linear integer arithmetic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the Twenty-Third International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 6803, pp. 338–353. Springer, Berlin (2011)

17.

Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Proceedings of the Sixth International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 7364, pp. 339–354. Springer, Berlin (2012)CrossRef

18.

Krstić, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson–Oppen with DPLL. In: Wolter, F. (ed.) Proceedings of the Sixth International Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 4720, pp. 1–27. Springer, Berlin (2007)

19.

Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76–82 (2009)CrossRef

20.

Marques Silva, J.P., 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, Amsterdam (2009)

21.

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

22.

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

23.

Zeljić, A., Wintersteiger, C.M., Rümmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) Proceedings of the Nineteenth International Conference on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 9710, pp. 249–266. Springer, Berlin (2016)

Title: Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness
Authors: Maria Paola Bonacina
Stéphane Graham-Lengrand
Natarajan Shankar
Publication date: 04-01-2019
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 3/2020
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-09510-y

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 3/2020

Strong Extension-Free Proof Systems

Scalable Fine-Grained Proofs for Formula Processing

Limited Second-Order Functionality in a First-Order Setting

Preface: Selected Extended Papers of CADE 2017

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

Preface to the Special Issue on Automated Reasoning Systems

Premium Partner