{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T07:34:35Z","timestamp":1672385675038},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1007\/s10472-009-9152-7","type":"journal-article","created":{"date-parts":[[2009,7,23]],"date-time":"2009-07-23T06:04:12Z","timestamp":1248329052000},"page":"63-99","source":"Crossref","is-referenced-by-count":9,"title":["Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis"],"prefix":"10.1007","volume":"55","author":[{"given":"Roberto","family":"Bruttomesso","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"Franzen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,7,24]]},"reference":[{"key":"9152_CR1","series-title":"LNCS","volume-title":"Proc. CAV\u201904","author":"T Ball","year":"2004","unstructured":"Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: automatic theorem proving for predicate abstraction refinement. In: Proc. CAV\u201904. LNCS, vol. 3114. Springer, New York (2004)"},{"key":"9152_CR2","series-title":"LNCS","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification (CAV \u201904)","author":"C Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: a new implementation of the cooperating validity checker. In: Proceedings of the 16th International Conference on Computer Aided Verification (CAV \u201904). LNCS, vol. 3114. Springer, New York (2004)"},{"key":"9152_CR3","series-title":"LNAI","volume-title":"Proc. LPAR\u201906","author":"C Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Proc. LPAR\u201906. LNAI, vol. 4246. Springer, New York (2006)"},{"key":"9152_CR4","series-title":"LNCS","volume-title":"Proc. CAV\u201907","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: Cvc3. In: Proc. CAV\u201907. LNCS, vol. 4590. Springer, New York (2007)"},{"key":"9152_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak\u2019s method for combining decision procedures. In: Frontiers of Combining Systems (FROCOS). Lecture Notes in Artificial Intelligence. Springer, Santa Margherita Ligure (2002)","DOI":"10.1007\/3-540-45988-X_11"},{"key":"9152_CR6","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Proc. of IJCAR\u201906. LNAI, no. 4130 (2006)","DOI":"10.1007\/11814771_42"},{"key":"9152_CR7","series-title":"ENTCS","volume-title":"Proc. PDPAR\u201905","author":"M Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Franzen, A., Hanna, Z., Khasidashvili, Z., Palti, A., Sebastiani, R.: Encoding RTL constructs for MathSAT: a preliminary report. In: Proc. PDPAR\u201905. ENTCS, vol. 144. Elsevier, Amsterdam (2006)"},{"key":"9152_CR8","series-title":"LNCS","volume-title":"Proc. TACAS\u201905","author":"M Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Proc. TACAS\u201905. LNCS, vol. 3440. Springer, New York (2005)"},{"key":"9152_CR9","series-title":"LNCS","volume-title":"Proc. CAV 2005","author":"M Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani,\u00a0R.: Efficient satisfiability modulo theories via delayed theory combination. In: Proc. CAV 2005. LNCS, vol. 3576. Springer, New York (2005)"},{"issue":"10","key":"9152_CR10","doi-asserted-by":"crossref","first-page":"1493","DOI":"10.1016\/j.ic.2005.05.011","volume":"204","author":"M Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani,\u00a0R.: Efficient theory combination via boolean search. Inf. Comput. 204(10), 1493\u20131525 (2006)","journal-title":"Inf. Comput."},{"key":"9152_CR11","first-page":"741","volume-title":"Proc. ASP-DAC 2002","author":"R Brinkmann","year":"2002","unstructured":"Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proc. ASP-DAC 2002, pp. 741\u2013746. IEEE, Piscataway (2002)"},{"key":"9152_CR12","series-title":"LNAI","volume-title":"Proc. LPAR\u201906","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: Proc. LPAR\u201906. LNAI, vol. 4246. Springer, New York (2006)"},{"key":"9152_CR13","series-title":"LNCS","volume-title":"CAV","author":"R Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franzen, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT solver. In: CAV. LNCS, vol. 5123. Springer, New York (2008)"},{"key":"9152_CR14","series-title":"LNCS","volume-title":"Proc. SAT\u201906","author":"S Cotton","year":"2006","unstructured":"Cotton, S., Maler, O.: Fast and flexible difference logic propagation for DPLL(T). In: Proc. SAT\u201906. LNCS, vol. 4121. Springer, New York (2006)"},{"key":"9152_CR15","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Model-based theory combination. In: Proc. of the 5th Workshop on Satisfiability Modulo Theories SMT\u201907. http:\/\/www.lsi.upc.edu\/~oliveras\/smt07\/ (2007)"},{"key":"9152_CR16","series-title":"LNCS","first-page":"218","volume-title":"Proc. IJCAR\u201904","author":"L Moura de","year":"2004","unstructured":"de\u00a0Moura, L., Owre, S., Ruess, H., Rushby, J., Shankar, N.: The ICS decision procedures for embedded deduction. In: Proc. IJCAR\u201904. LNCS, vol. 3097, pp. 218\u2013222. Springer, New York (2004)"},{"issue":"3","key":"9152_CR17","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"9152_CR18","series-title":"LNCS","volume-title":"Proc. CAV\u201906","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de\u00a0Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Proc. CAV\u201906. LNCS, vol. 4144. Springer, New York (2006)"},{"key":"9152_CR19","unstructured":"Dutertre, B., de\u00a0Moura, L.: System description: Yices 1.0. In: Proc. on 2nd SMT competition, SMT-COMP\u201906. yices.csl.sri.com\/yices-smtcomp06.pdf (2006)"},{"key":"9152_CR20","volume-title":"A Mathematical Introduction to Logic","author":"H Enderton","year":"1972","unstructured":"Enderton, H.: A Mathematical Introduction to Logic. Academic, London (1972)"},{"key":"9152_CR21","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Proc. CAV\u20192001 (2001)","DOI":"10.1007\/3-540-44585-4_22"},{"key":"9152_CR22","series-title":"LNCS","volume-title":"Proc. CAV 2003","author":"C Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Proc. CAV 2003. LNCS. Springer, New York (2003)"},{"key":"9152_CR23","series-title":"LNCS","volume-title":"Proc. LPAR\u201904","author":"P Fontaine","year":"2004","unstructured":"Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In: Proc. LPAR\u201904. LNCS, vol. 3452. Springer, New York (2004)"},{"key":"9152_CR24","series-title":"LNCS","first-page":"175","volume-title":"Proc. CAV\u201904","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Proc. CAV\u201904. LNCS, vol. 3114, pp. 175\u2013188. Springer, New York (2004)"},{"issue":"3","key":"9152_CR25","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/s10817-004-6241-5","volume":"33","author":"S Ghilardi","year":"2004","unstructured":"Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3), 221\u2013249 (2004)","journal-title":"J. Autom. Reason."},{"key":"9152_CR26","series-title":"LNCS","volume-title":"Proc. FroCos\u201905","author":"S Ghilardi","year":"2005","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. In: Proc. FroCos\u201905. LNCS, vol. 3717. Springer, New York (2005)"},{"key":"9152_CR27","series-title":"LNAI","volume-title":"Proc. Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007","author":"S Krstic","year":"2007","unstructured":"Krstic, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Proc. Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007. LNAI, vol. 4720. Springer, New York (2007)"},{"key":"9152_CR28","series-title":"LNCS","volume-title":"TACAS\u201907","author":"S Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: TACAS\u201907. LNCS, vol. 4424. Springer, New York (2007)"},{"key":"9152_CR29","series-title":"LNCS","volume-title":"Proc. of 5th International Workshop on Frontiers of Combining Systems (FroCos \u201905)","author":"SK Lahiri","year":"2005","unstructured":"Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Proc. of 5th International Workshop on Frontiers of Combining Systems (FroCos \u201905). LNCS, vol. 3717. Springer, New York (2005)"},{"issue":"2","key":"9152_CR30","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"CG Nelson","year":"1979","unstructured":"Nelson, C.G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245\u2013257 (1979)","journal-title":"TOPLAS"},{"key":"9152_CR31","series-title":"LNAI","first-page":"77","volume-title":"Proc. 10th LPAR","author":"R Nieuwenhuis","year":"2003","unstructured":"Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Proc. 10th LPAR. LNAI, no. 2850, pp. 77\u201389. Springer, New York (2003)"},{"key":"9152_CR32","series-title":"LNCS","volume-title":"Proc. CAV\u201905","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Proc. CAV\u201905. LNCS, vol. 3576. Springer, New York (2005)"},{"key":"9152_CR33","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comp. Sci. 12, 291\u2013302 (1980)","journal-title":"Theor. Comp. Sci."},{"key":"9152_CR34","series-title":"LNCS","volume-title":"Proc FroCos\u201905","author":"S Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Proc FroCos\u201905. LNCS, vol. 3717. Springer, New York (2005)"},{"key":"9152_CR35","volume-title":"Proc. LICS \u201901","author":"H Rue\u00df","year":"2001","unstructured":"Rue\u00df, H., Shankar, N.: Deconstructing Shostak. In: Proc. LICS \u201901. IEEE Computer Society, Piscataway (2001)"},{"key":"9152_CR36","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation, JSAT. 3, 141\u2013224 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation, JSAT"},{"key":"9152_CR37","doi-asserted-by":"crossref","unstructured":"Shankar, N., Rue\u00df, H.: Combining Shostak theories. Invited paper for Floc\u201902\/RTA\u201902 (2002)","DOI":"10.1007\/3-540-45610-4_1"},{"issue":"2","key":"9152_CR38","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/322123.322137","volume":"26","author":"R Shostak","year":"1979","unstructured":"Shostak, R.: A pratical decision procedure for arithmetic with function symbols. J. ACM 26(2), 51\u2013360 (1979)","journal-title":"J. ACM"},{"key":"9152_CR39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R Shostak","year":"1984","unstructured":"Shostak, R.: Deciding combinations of theories. J. ACM 31, 1\u201312 (1984)","journal-title":"J. ACM"},{"key":"9152_CR40","volume-title":"Proc. Frontiers of Combining Systems, FroCoS\u201906. Applied Logic","author":"C Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Proc. Frontiers of Combining Systems, FroCoS\u201906. Applied Logic. Kluwer, Dordrecht (1996)"},{"issue":"1","key":"9152_CR41","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C Tinelli","year":"2003","unstructured":"Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comp. Sci. 290(1), 291\u2013353 (2003)","journal-title":"Theor. Comp. Sci."},{"issue":"3","key":"9152_CR42","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.: Combining nonstably infinite theories. J. Autom. Reason. 34(3), 209\u2013238 (2005)","journal-title":"J. Autom. Reason."},{"key":"9152_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/3-540-45616-3_22","volume-title":"Proc. Tableaux\u201902","author":"CG Zarba","year":"2002","unstructured":"Zarba, C.G.: A tableau calculus for combining non-disjoint theories. In: Proc. Tableaux\u201902. Lecture Notes in Computer Science, vol. 2381, pp. 315\u2013329. Springer, New York (2002)"},{"key":"9152_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-45988-X_9","volume-title":"FroCos\u201902","author":"CG Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining sets with integers. In: FroCos\u201902. Lecture Notes in Computer Science, vol. 2309, pp. 103\u2013116. Springer, New York (2002)"},{"key":"9152_CR45","volume-title":"Proc. ICCAD \u201901","author":"L Zhang","year":"2001","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proc. ICCAD \u201901. IEEE, Piscataway (2001)"},{"key":"9152_CR46","series-title":"LNCS","first-page":"17","volume-title":"Proc. CAV\u201902","author":"L Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Proc. CAV\u201902. LNCS, no. 2404, pp. 17\u201336. Springer, New York (2002)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9152-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-009-9152-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9152-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T22:35:56Z","timestamp":1590014156000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-009-9152-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":46,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["9152"],"URL":"https:\/\/doi.org\/10.1007\/s10472-009-9152-7","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2]]}}}