Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs. (English) Zbl 07498608
Summary: Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform non-trivial inferences only when resolving conflicts between formulæ and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in unions of theories. It combines inference systems for individual theories as theory modules within a solver for the union of the theories. This article augments CDSAT with a more general lemma learning capability and with proof generation. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements for completeness and termination of CDSAT. Proof generation is accomplished by a proof-carrying version of the CDSAT transition system that produces proof objects in memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT the LCF approach to proofs from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 68R07 | Computational aspects of satisfiability |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
Keywords:
lemma learning; proof generation; satisfiability modulo theories; satisfiability modulo assignmentReferences:
| [1] | Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) Proceedings of the 1st International Conference on Certified Programs and Proofs (CPP), pp. 135-150. Springer (2011) · Zbl 1350.68223 |
| [2] | Barbosa, H.; Blanchette, JC; Fleury, M.; Fontaine, P., Scalable fine-grained proofs for formula processing, J. Autom. Reason., 64, 3, 485-550 (2020) · Zbl 1468.68278 · doi:10.1007/s10817-018-09502-y |
| [3] | Bjørner, N., de Moura, L.: Proofs and refutations, and Z3. In: Rudnick, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proc. 7th International Workshop on Implementation of Logics (IWIL), CEUR Workshop Proc., vol. 418, pp. 123-132 (2008) |
| [4] | Bjørner, N., Janota, M.: Playing with quantified satisfaction. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A. (eds.) Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)—Short Papers, EPiC Series in Computing, vol. 35, pp. 15-27. EasyChair (2015) |
| [5] | Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.), Proceedings of the 23rd International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 6803, pp. 116-130. Springer (2011) · Zbl 1314.68271 |
| [6] | Bobot, F., Graham-Lengrand, S., Marre, B., Bury, G.: Centralizing equality reasoning in MCSAT. In: D’Silva, V., Dimitrova, R. (eds.), Proceedings of the 16th Workshop on Satisfiability Modulo Theories (SMT) (2018) |
| [7] | Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.), Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP), Lecture Notes in Computer Science, vol. 6172, pp. 179-194. Springer (2010) · Zbl 1291.68328 |
| [8] | Bonacina, M.P.: On conflict-driven reasoning. In: Shankar, N., Dutertre, B. (eds.), Proceedings of the 6th Workshop on Automated Formal Methods (AFM), Kalpa Publications, vol. 5, pp. 31-49. EasyChair (2018) |
| [9] | Bonacina, M.P., Fontaine, P., Ringeissen, C., Tinelli, C.: Theory combination: beyond equality sharing. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A.Y. (eds.) Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader, Lecture Notes in Artificial Intelligence, vol. 11560, pp. 57-89. Springer (2019) · Zbl 1443.68116 |
| [10] | Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Proofs in conflict-driven theory combination. In: Andronick, J., Felty, A. (eds.), Proceedings of the 7th ACM International Conference on Certified Programs and Proofs (CPP), pp. 186-200. ACM Press (2018) |
| [11] | Bonacina, MP; Graham-Lengrand, S.; Shankar, N., Conflict-driven satisfiability for theory combination: transition system and completeness, J. Autom. Reason., 64, 3, 579-609 (2020) · Zbl 1468.68194 · doi:10.1007/s10817-018-09510-y |
| [12] | Bonacina, MP; Johansson, M., Interpolation systems for ground proofs in automated deduction: a survey, J. Autom. Reason., 54, 4, 353-390 (2015) · Zbl 1356.68179 · doi:10.1007/s10817-015-9325-5 |
| [13] | Bonacina, MP; Lynch, CA; de Moura, L., On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reason., 47, 2, 161-189 (2011) · Zbl 1243.68265 · doi:10.1007/s10817-010-9213-y |
| [14] | Bonacina, M.P., Mazzi, G.: The Eos SMT/SMA-solver: a preliminary report. In: Sharygina, N., Hendrix, J. (eds.), Proceedings of the 17th Workshop on Satisfiability Modulo Theories (SMT) (2019). http://smt2019.galois.com/proceedings.html |
| [15] | Bonacina, MP; Plaisted, DA, Semantically-guided goal-sensitive reasoning: inference system and completeness, J. Autom. Reason., 59, 2, 165-218 (2017) · Zbl 1437.68189 · doi:10.1007/s10817-016-9384-2 |
| [16] | Brauße, F., Korovin, K., Korovina, M., Müller, N.: A CDCL-style calculus for solving non-linear constraints. In: Herzig, A., Popescu, A. (eds.), Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS), Lecture Notes in Artificial Intelligence, vol. 11715, pp. 131-148. Springer (2019) · Zbl 1435.68300 |
| [17] | Bromberger, M., Sturm, T., Weidenbach, C.: Linear integer arithmetic revisited. In: Felty, A.P., Middeldorp, A. (eds.), Proceedings of the 25th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 9195, pp. 623-637. Springer (2015) · Zbl 1432.68596 |
| [18] | Chang, CL; Lee, RCT, Symbolic Logic and Mechanical Theorem Proving (1973), Cambridge: Academic Press, Cambridge · Zbl 0263.68046 |
| [19] | Cheney, J., Hinze, R.: First-Class Phantom Types. Tech. Rep. CUCIS TR2003-1901, Cornell University, Ithaca, NY, USA (2003) |
| [20] | Chocron, P.; Fontaine, P.; Ringeissen, C., Politeness and combination methods for theories with bridging functions, J. Autom. Reason., 64, 1, 97-134 (2020) · Zbl 1468.68143 · doi:10.1007/s10817-019-09512-4 |
| [21] | Cotton, S.: Natural domain SMT: a preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.), Proceedings of the 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science, vol. 6246, pp. 77-91. Springer (2010) · Zbl 1290.68112 |
| [22] | Cruz-Felipe, L., Heule, M., Hunt Jr., W., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.), Proceedings of the 26th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 10395, pp. 220-236. Springer (2017) · Zbl 1494.68284 |
| [23] | de Moura, L., Bjørner, N.: Model-based theory combination. In: Krstić, S., Oliveras, A. (eds.), Proceedings of the 5th Workshop on Satisfiability Modulo Theories (SMT 2007), Electronic Notes in Theoretical Computer Science, vol. 198(2), pp. 37-49. Elsevier (2008) · Zbl 1277.03007 |
| [24] | de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.), Proceedings of the 14th Internatinal Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), Lecture Notes in Computer Science, vol. 7737, pp. 1-12. Springer (2013) · Zbl 1426.68251 |
| [25] | Dutertre, B.: Yices 2.2. In: A. Biere, R. Bloem (eds.), Proceedings of the 26th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 8559, pp. 737-744. Springer (2014) |
| [26] | Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.), Proceedings of the 18th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 4144, pp. 81-94. Springer (2006) |
| [27] | Fontaine, P., Marion, J.Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.), Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 3920, pp. 167-181. Springer (2006) · Zbl 1180.68240 |
| [28] | Ghilardi, S.; Nicolini, E.; Zucchelli, D., A comprehensive combination framework, ACM Trans. Comput. Log., 9, 2, 1-54 (2008) · Zbl 1407.03011 · doi:10.1145/1342991.1342992 |
| [29] | Goldberg, E.Y., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the Conference on Design Automation and Test in Europe (DATE), pp. 10886-10891. IEEE (2003) |
| [30] | Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanized Logic of Computation. Lecture Notes in Computer Science, vol. 78. Springer (1979) · Zbl 0421.68039 |
| [31] | Graham-Lengrand, S., Jovanović, D., Dutertre, B.: Solving bitvectors with MCSAT: explanations from bits and pieces. In: Peltier, N., Sofronie-Stokkermans, V. (eds.), Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Artificial Intelligence, vol. 12166, pp. 103-121. Springer (2020) · Zbl 07614509 |
| [32] | Heule, M., Hunt Jr., W., Wetzler, N.: Verifying resolutions with extended refutation. In: Bonacina, M.P. (ed.), Proceedings of the 24th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 7898, pp. 345-359. Springer (2013) · Zbl 1381.68270 |
| [33] | Järvisalo, M., Heule, M., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.), Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Artificial Intelligence, vol. 7364, pp. 355-370. Springer (2012) · Zbl 1358.68256 |
| [34] | Jovanović, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) Proceedings of the 18th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), Lecture Notes in Computer Science, vol. 10145, pp. 330-346. Springer (2017) · Zbl 1484.68220 |
| [35] | 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 13th International Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE (2013) |
| [36] | Jovanović, D.; de Moura, L., Cutting to the chase: solving linear integer arithmetic, J. Autom. Reason., 51, 79-108 (2013) · Zbl 1314.90053 · doi:10.1007/s10817-013-9281-x |
| [37] | Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.), Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Artificial Intelligence, vol. 7364, pp. 339-354. Springer (2012) · Zbl 1358.68257 |
| [38] | Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.), Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 93-100. ACM and IEEE (2016) |
| [39] | Klee, V., Minty, G.J.: How good is the simplex algorithm? In: O. Shisha (ed.) Inequalities—III, pp. 159-175. Academic Press (1972) · Zbl 0297.90047 |
| [40] | Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: I.P. Gent (ed.), Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming (CP), Lecture Notes in Computer Science, vol. 5732, pp. 509-523. Springer (2009) · Zbl 1336.68236 |
| [41] | Kroening, D., Strichman, O.: Decision Procedures—An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer (2008) · Zbl 1149.68071 |
| [42] | Krstić, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: F. Wolter (ed.), Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS), Lecture Notes in Artificial Intelligence, vol. 4720, pp. 1-27. Springer (2007) · Zbl 1148.68466 |
| [43] | Lassez, JL; Maher, MJ, On Fourier’s algorithm for linear arithmetic constraints, J. Autom. Reason., 9, 373-379 (1992) · Zbl 0781.90064 · doi:10.1007/BF00245296 |
| [44] | 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) · Zbl 1183.68568 |
| [45] | Marques Silva, JP; Sakallah, KA, GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 5, 506-521 (1999) · Zbl 1392.68388 · doi:10.1109/12.769433 |
| [46] | McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.), Proceedings of the 21st International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 5643, pp. 462-476. Springer (2009) · Zbl 1242.68282 |
| [47] | Milner, R.: LCF: a way of doing proofs with a machine. In: Becvár, J. (ed.) Proceedings of the 8th International Symposium on Mathematical Foundations of Computer Science (MFCS), Lecture Notes in Computer Science, vol. 74, pp. 146-159. Springer (1979) · Zbl 0423.68049 |
| [48] | Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201-211. American Mathematical Society (1983) · Zbl 0564.03011 |
| [49] | Nelson, G.; Oppen, DC, Simplification by cooperating decision procedures, ACM Trans. Prog. Lang. Syst., 1, 2, 245-257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079 |
| [50] | 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) · Zbl 1326.68164 · doi:10.1145/1217856.1217859 |
| [51] | Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Claessen, K., Kuncak, V. (eds.) Proceedings of the 14th Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE (2014) |
| [52] | Schrijver, A.: Theory of Linear and Integer Programming. Interscience Series in Discrete Mathematics and Optimization. Wiley (1998) · Zbl 0970.90052 |
| [53] | Shankar, N.: Trust and automation in verification tools. In: Cha, S.S., Choi, J.Y., Kim, M., Lee, I., Viswanathan, M. (eds.) Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 5311, pp. 4-17. Springer (2008) |
| [54] | Spielman, D.A., Teng, S.H.: Smoothed analysis of algorithms: why the simplex algorithm normally takes polynomial time. In: Proceedings of the 33rd Annual ACM Symp. on the Theory of Computing (STOC), pp. 296-305. ACM Press (2001). Long version available at arXiv:cs/0111050v7 [cs.DS] 9 Oct. 2003 · Zbl 1323.68636 |
| [55] | Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Aiken, A., Morrisett, G. (eds.) Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 224-235. ACM Press (2003) · Zbl 1321.68161 |
| [56] | Zeljić, A., Wintersteiger, C.M., Rümmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 9710, pp. 249-266. Springer (2016) · Zbl 1475.68226 |
| [57] | Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the Conference on Design Automation and Test in Europe (DATE), pp. 10880-10885. IEEE (2003) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
