{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:50:59Z","timestamp":1781927459635,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540746201","type":"print"},{"value":"9783540746218","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74621-8_2","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T11:46:32Z","timestamp":1187783192000},"page":"28-46","source":"Crossref","is-referenced-by-count":2,"title":["From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Sebastiani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 1999","author":"A. Armando","year":"1999","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Jaffar, J. (ed.) Principles and Practice of Constraint Programming \u2013 CP 1999. LNCS, vol.\u00a01713, Springer, Heidelberg (1999)"},{"issue":"3\u20134","key":"2_CR2","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/BF01530803","volume":"8","author":"A. Armando","year":"1993","unstructured":"Armando, A., Giunchiglia, E.: Embedding Complex Decision Procedures inside an Interactive Theorem Prover. Annals of Mathematics and Artificial Intelligence\u00a08(3\u20134), 475\u2013502 (1993)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2_CR3","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Korni\u0142owicz, A., Sebastiani, R.: A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, Springer, Heidelberg (2002)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Dill, D., Stump, A.: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In: 14th International Conference on Computer-Aided Verification (2002)","DOI":"10.1007\/3-540-45657-0_18"},{"key":"2_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Barrett","year":"2006","unstructured":"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.\u00a04246, Springer, Heidelberg (2006)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: MathSAT: A Tight Integration of SAT and Mathematical Decision Procedure. Journal of Automated Reasoning\u00a035(1-3) (2005)","DOI":"10.1007\/s10817-005-9004-z"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P.: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient Theory Combination via Boolean Search. Information and Computation\u00a0204(10) (2006)","DOI":"10.1016\/j.ic.2005.05.011"},{"key":"2_CR9","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Bruttomesso","year":"2006","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, Springer, Heidelberg (2006)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S. Cotton","year":"2006","unstructured":"Cotton, S., Maler, O.: Fast and Flexible Difference Logic Propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, Springer, Heidelberg (2006)"},{"issue":"3","key":"2_CR11","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M. D\u2019Agostino","year":"1994","unstructured":"D\u2019Agostino, M., Mondadori, M.: The Taming of the Cut. Journal of Logic and Computation\u00a04(3), 285\u2013319 (1994)","journal-title":"Journal of Logic and Computation"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Davis, M., Longemann, G., Loveland, D.: A machine program for theorem proving. Journal of the ACM\u00a05(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"2_CR14","unstructured":"de Moura, L., Bjorner, N.: Model-based Theory Combination. In: Proc. 5th workshop on Satisfiability Modulo Theories, SMT 2007 (to appear, 2007)"},{"key":"2_CR15","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lemmas on Demand for Satisfiability Solvers. In: Proc. SAT 2002 (2002)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"2_CR17","unstructured":"Dutertre, B., de Moura, L.: System Description: Yices 1.0. In: Proc. on 2nd SMT competition, SMT-COMP\u201906 (2006), Available at yices.csl.sri.com\/yices-smtcomp06.pdf"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem Proving Using Lazy Proof Explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, Springer, Heidelberg (2003)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"},{"key":"2_CR20","unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R., Tacchella, A.: More evaluation of decision procedures for modal logics. In: Proc. KR 1998, Trento, Italy (1998)"},{"issue":"2","key":"2_CR21","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1080\/11663081.2000.10510994","volume":"10","author":"E. Giunchiglia","year":"2000","unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R., Tacchella, A.: SAT vs. Translation based decision procedures for modal logics: a comparative evaluation. Journal of Applied Non-Classical Logics\u00a010(2), 145\u2013172 (2000)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2_CR22","unstructured":"Giunchiglia, E., Giunchiglia, F., Tacchella, A.: SAT Based Decision Procedures for Classical Modal Logics. Journal of Automated Reasoning. Special Issue: Satisfiability at the start of the year 2000 (2001)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In: CADE 1996. LNCS (LNAI), Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61511-3_115"},{"key":"2_CR24","unstructured":"Giunchiglia, F., Sebastiani, R.: A SAT-based decision procedure for ALC. In: Proc. KR 1996, Cambridge, MA, USA (November 1996)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K(m). Information and Computation\u00a0162(1\/2) (2000)","DOI":"10.1006\/inco.1999.2850"},{"key":"2_CR26","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","author":"V. Haarslev","year":"2001","unstructured":"Haarslev, V., Moeller, R.: RACER System Description. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, Springer, Heidelberg (2001)"},{"key":"2_CR27","unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: 6th International Conference on Principles of Knowledge Representation and Reasoning (KR 1998), pp. 636\u2013647 (1998)"},{"issue":"3","key":"2_CR28","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Patel-Schneider, P.F.: Optimizing Description Logic Subsumption. Journal of Logic and Computation\u00a09(3), 267\u2013293 (1999)","journal-title":"Journal of Logic and Computation"},{"issue":"3","key":"2_CR29","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1093\/jigpal\/8.3.293","volume":"8","author":"I. Horrocks","year":"2000","unstructured":"Horrocks, I., Patel-Schneider, P.F., Sebastiani, R.: An Analysis of Empirical Testing for Modal Decision Procedures. Logic Journal of the IGPL\u00a08(3), 293\u2013323 (2000)","journal-title":"Logic Journal of the IGPL"},{"key":"2_CR30","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"FroCos 2005","author":"S.K. Lahiri","year":"2005","unstructured":"Lahiri, S.K., Musuvathi, M.: An Efficient Decision Procedure for UTVPI Constraints. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, Springer, Heidelberg (2005)"},{"issue":"2","key":"2_CR31","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. on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/11532231","volume-title":"Term Rewriting and Applications","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-Producing Congruence Closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, Springer, Heidelberg (2005)"},{"issue":"6","key":"2_CR33","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). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theoretical Computer Science\u00a012, 291\u2013302 (1980)","journal-title":"Theoretical Computer Science"},{"key":"2_CR35","unstructured":"Patel-Schneider, P.F.: DLP System Description. In: Proc. Int. Workshop on Description Logics. In: DL 1998 (1998)"},{"key":"2_CR36","unstructured":"Sebastiani, R.: Lazy Satisfiability Modulo Theories. Technical Report dtr-07-022, DIT, University of Trento, Italy (April 2007), Available at http:\/\/eprints.biblio.unitn.it\/archive\/00001196\/01\/dtr-07-022.pdf"},{"key":"2_CR37","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0057460","volume-title":"Artificial Intelligence: Methodology, Systems, and Applications","author":"R. Sebastiani","year":"1998","unstructured":"Sebastiani, R., Villafiorita, A.: SAT-based decision procedures for normal modal logics: a theoretical framework. In: Giunchiglia, F. (ed.) AIMSA 1998. LNCS (LNAI), vol.\u00a01480, Springer, Heidelberg (1998)"},{"key":"2_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding Combinations of Theories. Journal of the ACM\u00a031, 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"key":"2_CR39","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)"},{"key":"2_CR40","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-45757-7_26","volume-title":"Logics in Artificial Intelligence","author":"C. Tinelli","year":"2002","unstructured":"Tinelli, C.: A DPLL-based Calculus for Ground Satisfiability Modulo Theories. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol.\u00a02424, pp. 308\u2013319. Springer, Heidelberg (2002)"},{"key":"2_CR41","unstructured":"Wolfman, S., Weld, D.: The LPSAT Engine & its Application to Resource Planning. In: Proc. IJCAI (1999)"},{"key":"2_CR42","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD, pp. 279\u2013285 (2001)"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-45657-0_2","volume-title":"Computer Aided Verification","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 17\u201336. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74621-8_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:30:42Z","timestamp":1619519442000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74621-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540746201","9783540746218"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}