{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:28:31Z","timestamp":1750670911674,"version":"3.37.3"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,9,12]],"date-time":"2021-09-12T00:00:00Z","timestamp":1631404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,9,12]],"date-time":"2021-09-12T00:00:00Z","timestamp":1631404800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1528153","CNS-0917375"],"award-info":[{"award-number":["1528153","CNS-0917375"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007052","name":"Universit\u00e0 degli Studi di Verona","doi-asserted-by":"publisher","award":["\u201cRicerca di base 2017\u201d"],"award-info":[{"award-number":["\u201cRicerca di base 2017\u201d"]}],"id":[{"id":"10.13039\/501100007052","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-C-0043"],"award-info":[{"award-number":["FA8750-16-C-0043"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<jats:italic>Conflict-driven<\/jats:italic>procedures perform non-trivial inferences only when resolving conflicts between formul\u00e6 and assignments representing the candidate model. CDSAT (<jats:italic>Conflict-Driven SATisfiability<\/jats:italic>) is a method for conflict-driven reasoning in<jats:italic>unions of theories<\/jats:italic>. It combines inference systems for individual theories as<jats:italic>theory modules<\/jats:italic>within a solver for the union of the theories. This article augments CDSAT with a more general<jats:italic>lemma learning<\/jats:italic>capability and with<jats:italic>proof generation<\/jats:italic>. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements for<jats:italic>completeness<\/jats:italic>and<jats:italic>termination<\/jats:italic>of CDSAT. Proof generation is accomplished by a<jats:italic>proof-carrying<\/jats:italic>version of the CDSAT transition system that produces<jats:italic>proof objects<\/jats:italic>in memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT the<jats:italic>LCF approach to proofs<\/jats:italic>from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.<\/jats:p>","DOI":"10.1007\/s10817-021-09606-y","type":"journal-article","created":{"date-parts":[[2021,9,12]],"date-time":"2021-09-12T18:02:46Z","timestamp":1631469766000},"page":"43-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9104-2692","authenticated-orcid":false,"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[]},{"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"additional","affiliation":[]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,9,12]]},"reference":[{"key":"9606_CR1","doi-asserted-by":"crossref","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, 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\u2013150. Springer (2011)","DOI":"10.1007\/978-3-642-25379-9_12"},{"issue":"3","key":"9606_CR2","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10817-018-09502-y","volume":"64","author":"H Barbosa","year":"2020","unstructured":"Barbosa, H., Blanchette, J.C., Fleury, M., Fontaine, P.: Scalable fine-grained proofs for formula processing. J. Autom. Reason. 64(3), 485\u2013550 (2020)","journal-title":"J. Autom. Reason."},{"key":"9606_CR3","unstructured":"Bj\u00f8rner, 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\u2013132 (2008)"},{"key":"9606_CR4","unstructured":"Bj\u00f8rner, 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)\u2014Short Papers, EPiC Series in Computing, vol.\u00a035, pp. 15\u201327. EasyChair (2015)"},{"key":"9606_CR5","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.), Proceedings of the 23rd International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, vol. 6803, pp. 116\u2013130. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"9606_CR6","unstructured":"Bobot, F., Graham-Lengrand, S., Marre, B., Bury, G.: Centralizing equality reasoning in MCSAT. In: D\u2019Silva, V., Dimitrova, R. (eds.), Proceedings of the 16th Workshop on Satisfiability Modulo Theories (SMT) (2018)"},{"key":"9606_CR7","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, 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\u2013194. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"9606_CR8","doi-asserted-by":"crossref","unstructured":"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.\u00a05, pp. 31\u201349. EasyChair (2018)","DOI":"10.29007\/spwm"},{"key":"9606_CR9","doi-asserted-by":"crossref","unstructured":"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\u201389. Springer (2019)","DOI":"10.1007\/978-3-030-22102-7_3"},{"key":"9606_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013200. ACM Press (2018)","DOI":"10.1145\/3167096"},{"issue":"3","key":"9606_CR11","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/s10817-018-09510-y","volume":"64","author":"MP Bonacina","year":"2020","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: transition system and completeness. J. Autom. Reason. 64(3), 579\u2013609 (2020)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9606_CR12","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/s10817-015-9325-5","volume":"54","author":"MP Bonacina","year":"2015","unstructured":"Bonacina, M.P., Johansson, M.: Interpolation systems for ground proofs in automated deduction: a survey. J. Autom. Reason. 54(4), 353\u2013390 (2015)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9606_CR13","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161\u2013189 (2011)","journal-title":"J. Autom. Reason."},{"key":"9606_CR14","unstructured":"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"},{"issue":"2","key":"9606_CR15","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s10817-016-9384-2","volume":"59","author":"MP Bonacina","year":"2017","unstructured":"Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: inference system and completeness. J. Autom. Reason. 59(2), 165\u2013218 (2017)","journal-title":"J. Autom. Reason."},{"key":"9606_CR16","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Korovin, K., Korovina, M., M\u00fcller, 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\u2013148. Springer (2019)","DOI":"10.1007\/978-3-030-29007-8_8"},{"key":"9606_CR17","doi-asserted-by":"crossref","unstructured":"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\u2013637. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_42"},{"key":"9606_CR18","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"CL Chang","year":"1973","unstructured":"Chang, C.L., Lee, R.C.T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Cambridge (1973)"},{"key":"9606_CR19","unstructured":"Cheney, J., Hinze, R.: First-Class Phantom Types. Tech. Rep. CUCIS TR2003-1901, Cornell University, Ithaca, NY, USA (2003)"},{"issue":"1","key":"9606_CR20","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10817-019-09512-4","volume":"64","author":"P Chocron","year":"2020","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: Politeness and combination methods for theories with bridging functions. J. Autom. Reason. 64(1), 97\u2013134 (2020)","journal-title":"J. Autom. Reason."},{"key":"9606_CR21","doi-asserted-by":"crossref","unstructured":"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\u201391. Springer (2010)","DOI":"10.1007\/978-3-642-15297-9_8"},{"key":"9606_CR22","doi-asserted-by":"crossref","unstructured":"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\u2013236. Springer (2017)","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"9606_CR23","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based theory combination. In: Krsti\u0107, 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\u201349. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.04.079"},{"key":"9606_CR24","unstructured":"de Moura, L., Jovanovi\u0107, 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\u201312. Springer (2013)"},{"key":"9606_CR25","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: A.\u00a0Biere, R.\u00a0Bloem (eds.), Proceedings of the 26th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 8559, pp. 737\u2013744. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"9606_CR26","doi-asserted-by":"crossref","unstructured":"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\u201394. Springer (2006)","DOI":"10.1007\/11817963_11"},{"key":"9606_CR27","doi-asserted-by":"crossref","unstructured":"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\u2013181. Springer (2006)","DOI":"10.1007\/11691372_11"},{"issue":"2","key":"9606_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1342991.1342992","volume":"9","author":"S Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM Trans. Comput. Log. 9(2), 1\u201354 (2008)","journal-title":"ACM Trans. Comput. Log."},{"key":"9606_CR29","unstructured":"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\u201310891. IEEE (2003)"},{"key":"9606_CR30","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanized Logic of Computation. Lecture Notes in Computer Science, vol. 78. Springer (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"9606_CR31","doi-asserted-by":"crossref","unstructured":"Graham-Lengrand, S., Jovanovi\u0107, 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\u2013121. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_7"},{"key":"9606_CR32","doi-asserted-by":"crossref","unstructured":"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\u2013359. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"9606_CR33","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, 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\u2013370. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"9606_CR34","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, 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\u2013346. Springer (2017)","DOI":"10.1007\/978-3-319-52234-0_18"},{"key":"9606_CR35","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C., de\u00a0Moura, 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)","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"9606_CR36","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, D., de Moura, L.: Cutting to the chase: solving linear integer arithmetic. J. Autom. Reason. 51, 79\u2013108 (2013)","journal-title":"J. Autom. Reason."},{"key":"9606_CR37","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., de\u00a0Moura, 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\u2013354. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"9606_CR38","doi-asserted-by":"crossref","unstructured":"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\u2013100. ACM and IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"9606_CR39","unstructured":"Klee, V., Minty, G.J.: How good is the simplex algorithm? In: O.\u00a0Shisha (ed.) Inequalities\u2014III, pp. 159\u2013175. Academic Press (1972)"},{"key":"9606_CR40","doi-asserted-by":"crossref","unstructured":"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\u2013523. Springer (2009)","DOI":"10.1007\/978-3-642-04244-7_41"},{"key":"9606_CR41","unstructured":"Kroening, D., Strichman, O.: Decision Procedures\u2014An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer (2008)"},{"key":"9606_CR42","doi-asserted-by":"crossref","unstructured":"Krsti\u0107, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: F.\u00a0Wolter (ed.), Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS), Lecture Notes in Artificial Intelligence, vol. 4720, pp. 1\u201327. Springer (2007)","DOI":"10.1007\/978-3-540-74621-8_1"},{"key":"9606_CR43","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/BF00245296","volume":"9","author":"JL Lassez","year":"1992","unstructured":"Lassez, J.L., Maher, M.J.: On Fourier\u2019s algorithm for linear arithmetic constraints. J. Autom. Reason. 9, 373\u2013379 (1992)","journal-title":"J. Autom. Reason."},{"key":"9606_CR44","unstructured":"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\u2013153. IOS Press (2009)"},{"issue":"5","key":"9606_CR45","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques Silva","year":"1999","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"9606_CR46","doi-asserted-by":"crossref","unstructured":"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\u2013476. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_35"},{"key":"9606_CR47","doi-asserted-by":"crossref","unstructured":"Milner, R.: LCF: a way of doing proofs with a machine. In: Becv\u00e1r, J. (ed.) Proceedings of the 8th International Symposium on Mathematical Foundations of Computer Science (MFCS), Lecture Notes in Computer Science, vol.\u00a074, pp. 146\u2013159. Springer (1979)","DOI":"10.1007\/3-540-09526-8_11"},{"key":"9606_CR48","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201\u2013211. American Mathematical Society (1983)","DOI":"10.1090\/conm\/029\/11"},{"issue":"2","key":"9606_CR49","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Prog. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"issue":"6","key":"9606_CR50","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"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\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9606_CR51","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"9606_CR52","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Interscience Series in Discrete Mathematics and Optimization. Wiley (1998)"},{"key":"9606_CR53","unstructured":"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\u201317. Springer (2008)"},{"key":"9606_CR54","unstructured":"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\u2013305. ACM Press (2001). Long version available at arXiv:cs\/0111050v7 [cs.DS] 9 Oct. 2003"},{"key":"9606_CR55","doi-asserted-by":"crossref","unstructured":"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\u2013235. ACM Press (2003)","DOI":"10.1145\/640128.604150"},{"key":"9606_CR56","doi-asserted-by":"crossref","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, 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\u2013266. Springer (2016)","DOI":"10.1007\/978-3-319-40970-2_16"},{"key":"9606_CR57","unstructured":"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\u201310885. IEEE (2003)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09606-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09606-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09606-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T06:49:52Z","timestamp":1725778192000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09606-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,12]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["9606"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09606-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2021,9,12]]},"assertion":[{"value":"18 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 August 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 September 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}