{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:47:15Z","timestamp":1725472035512},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540482819"},{"type":"electronic","value":"9783540482826"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11916277_36","type":"book-chapter","created":{"date-parts":[[2006,10,17]],"date-time":"2006-10-17T18:32:59Z","timestamp":1161109979000},"page":"527-541","source":"Crossref","is-referenced-by-count":5,"title":["Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis"],"prefix":"10.1007","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":"Franz\u00e9n","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","reference":[{"key":"36_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11527695_2","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Armando","year":"2005","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 16\u201329. Springer, Heidelberg (2005)"},{"key":"36_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"36_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/11513988_34","volume-title":"Computer Aided Verification","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 335\u2013349. Springer, Heidelberg (2005)"},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., van Rossum, P., Schulz, S., Sebastiani, R.: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 317\u2013333. Springer, Heidelberg (2005)"},{"key":"36_CR5","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 (to appear, 2005)","DOI":"10.1007\/s10817-005-9004-z"},{"key":"36_CR6","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 (to appear, 2005)","DOI":"10.1016\/j.ic.2005.05.011"},{"key":"36_CR7","doi-asserted-by":"crossref","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. Technical Report DIT-06-032, DIT, University of Trento (2006), Available at: http:\/\/dit.unitn.it\/~rseba\/papers\/lpar06_dtc_extended.pdf","DOI":"10.1007\/11916277_36"},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some Progress in Satisfiability Checking for Difference Logic. In: Proc. FORMATS-FTRTFT 2004 (2004)","DOI":"10.1007\/978-3-540-30206-3_19"},{"key":"36_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"36_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","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, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"issue":"2","key":"36_CR11","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":"36_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/3-540-44881-0","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2003","unstructured":"Nieuwenhuis, R., Oliveras, A.: Congruence Closure with Integer Offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 77\u201389. Springer, Heidelberg (2003)"},{"key":"36_CR13","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":"36_CR14","volume-title":"Proc. ICCAD 2001","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 2001. IEEE Press, Los Alamitos (2001)"},{"key":"36_CR15","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","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11916277_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:58:20Z","timestamp":1605643100000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11916277_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540482819","9783540482826"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11916277_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}