{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:37:39Z","timestamp":1781239059279,"version":"3.54.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2005,10,1]],"date-time":"2005-10-01T00:00:00Z","timestamp":1128124800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2005,10]]},"DOI":"10.1007\/s10817-005-9004-z","type":"journal-article","created":{"date-parts":[[2005,12,8]],"date-time":"2005-12-08T09:13:49Z","timestamp":1134033229000},"page":"265-293","source":"Crossref","is-referenced-by-count":39,"title":["MathSAT: Tight Integration of SAT and Mathematical Decision Procedures"],"prefix":"10.1007","volume":"35","author":[{"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roberto","family":"Bruttomesso","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tommi","family":"Junttila","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"van Rossum","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,12,9]]},"reference":[{"key":"9004_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C. and Giunchiglia, E.: SAT-based procedures for temporal reasoning, in Proc. European Conference on Planning, CP-99.","DOI":"10.1007\/10720246_8"},{"key":"9004_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C., Giunchiglia, E. and Maratea, M.: A SAT-based decision procedure for the boolean combination of difference constraints, in Proc. Conference on Theory and Applications of Satisfiability Testing (SAT'04), 2004.","DOI":"10.1007\/11527695_2"},{"key":"9004_CR3","doi-asserted-by":"crossref","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A. and Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions, in Proc. CADE'2002, Vol. 2392 of LNAI, 2002.","DOI":"10.1007\/3-540-45620-1_17"},{"key":"9004_CR4","unstructured":"Audemard, G., Cimatti, A., Kornilowicz, A. and Sebastiani, R.: SAT-based bounded model checking for timed systems, in Proc. FORTE'02, Vol. 2529 of LNCS, 2002."},{"key":"9004_CR5","unstructured":"Badros, G. and Borning, A.: The Cassowary linear arithmetic constraint solving algorithm: interface and implementation. Technical Report UW-CSE-98-06-04, University of Washington, 1998."},{"key":"9004_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Lahiri, S. and Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement, in Proc. CAV'04, Vol. 3114 of LNCS, 2004, pp. 457\u2013461.","DOI":"10.1007\/978-3-540-27813-9_36"},{"key":"9004_CR7","doi-asserted-by":"crossref","unstructured":"Barrett, C. and Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker, in Proc. CAV'04, Vol. 3114 of LNCS, 2004, pp. 515\u2013518.","DOI":"10.1007\/978-3-540-27813-9_49"},{"key":"9004_CR8","unstructured":"Bayardo, Jr., R. J. and Schrag, R. C.: Using CSP look-back techniques to solve real-world SAT instances, in Proc. AAAI\/IAAI'97, 1997, pp. 203\u2013208."},{"key":"9004_CR9","doi-asserted-by":"crossref","unstructured":"Bockmayr, A. and Weispfenning, V.: Solving numerical constraints, in Handbook of Automated Reasoning, MIT, 2001, pp. 751\u2013842.","DOI":"10.1016\/B978-044450813-3\/50014-X"},{"key":"9004_CR10","doi-asserted-by":"crossref","unstructured":"Borning, A., Marriott, K., Stuckey, P. and Xiao, Y.: Solving linear arithmetic constraints for user interface applications, in Proc. UIST'97, 1997, pp. 87\u201396.","DOI":"10.1145\/263407.263518"},{"key":"9004_CR11","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S. and Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic, in Proc. TACAS 2005, Vol. 3440 of LNCS, 2005, pp. 317\u2013333.","DOI":"10.1007\/978-3-540-31980-1_21"},{"key":"9004_CR12","doi-asserted-by":"crossref","unstructured":"Brinkmann, R. and Drechsler, R.: RTL-Datapath verification using integer linear programming, in Proc. ASP-DAC 2002, 2002, pp. 741\u2013746.","DOI":"10.1109\/ASPDAC.2002.995022"},{"key":"9004_CR13","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/s101070050058","volume":"85","author":"B. Cherkassky","year":"1999","unstructured":"Cherkassky, B. and Goldberg, A.: Negative-cycle detection algorithms, Math. Program. 85 (1999), 277\u2013311.","journal-title":"Math. Program."},{"key":"9004_CR14","doi-asserted-by":"crossref","unstructured":"Cotton, S., Asarin, E., Maler, O. and 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":"9004_CR15","unstructured":"CVC. CVC, CVCLite and SVC. http:\/\/verify.stanford.edu\/ {CVC, CVCL, SVC}."},{"key":"9004_CR16","unstructured":"de Moura, L. and Ruess, H.: An experimental evaluation of ground decision procedures, in R. Alur and D. Peled (eds.), Proc. 15th Int. Conf. on Computer Aided Verification-CAV04, Vol. 3114 of LNCS. Boston, Massachusetts, 2004, pp. 162\u2013174."},{"key":"9004_CR17","unstructured":"E\u00e9n, N. and S\u00f6rensson, N.: An extensible SAT-solver, in Theory and Applications of Satisfiability Testing (SAT 2003), Vol. 2919 of LNCS, 2004, pp. 502\u2013518."},{"key":"9004_CR18","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Ruess, H. and Shankar, N.: ICS: Integrated canonizer and solver, in Proc. CAV'01, Vol. 2102 of LNCS, 2001, pp. 246\u2013249.","DOI":"10.1007\/3-540-44585-4_22"},{"key":"9004_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Joshi, R., Ou, X. and Saxe, J.: Theorem proving using lazy proof explication, in Proc. CAV'03, Vol. 2725 of LNCS, 2003, pp. 355\u2013367.","DOI":"10.1007\/978-3-540-45069-6_34"},{"key":"9004_CR20","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A. and Tinelli, C.: DPLL(T): fast decision procedures, in Proc. CAV'04, Vol. 3114 of LNCS, 2004, pp. 175\u2013188.","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"9004_CR21","unstructured":"GMP. GNU Multi Precision Library. http:\/\/www.swox.com\/gmp ."},{"key":"9004_CR22","unstructured":"Gomes, C., Selman, B. and Kautz, H.: Boosting combination search through randomization, in Proc. of the Fifteenth National Conf. on Artificial Intelligence, 1998, pp. 431\u2013437."},{"key":"9004_CR23","unstructured":"ICS. ICS. http:\/\/www.icansolve.com ."},{"issue":"3","key":"9004_CR24","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1145\/129393.129398","volume":"14","author":"J. Jaffar","year":"1992","unstructured":"Jaffar, J., Michaylov, S., Stuckey, P.J. and Yap, R.H.C.: The CLP(R) languages and systems, ACM Trans. Program. Lang. Syst. (TOPLAS) 14(3) (1992), 339\u2013395.","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"9004_CR25","doi-asserted-by":"crossref","unstructured":"Kroening, D., Ouaknine, J., Seshia, S. and Strichman, O.: Abstraction-based satisfiability solving of Presburger arithmetic, in Proc. CAV'04, Vol. 3114 of LNCS, 2004, pp. 308\u2013320.","DOI":"10.1007\/978-3-540-27813-9_24"},{"key":"9004_CR26","doi-asserted-by":"crossref","first-page":"497","DOI":"10.2307\/1910129","volume":"28","author":"H. Land","year":"1960","unstructured":"Land, H. and Doig, A.: An automatic method for solving discrete programming problems, Econometrica 28 (1960), 497\u2013520.","journal-title":"Econometrica"},{"key":"9004_CR27","unstructured":"MATHSAT. MathSAT. http:\/\/mathsat.itc.it ."},{"key":"9004_CR28","doi-asserted-by":"crossref","unstructured":"Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L. and Malik, S.: Chaff engineering an efficient SAT solver, in Proc. DAC'01, 2001, pp. 530\u2013535.","DOI":"10.1145\/378239.379017"},{"key":"9004_CR29","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R. and Oliveras, A.: Congruence closure with integer offset, in Proc. 10th LPAR, 2003, pp. 77\u201389.","DOI":"10.1007\/978-3-540-39813-4_5"},{"key":"9004_CR30","unstructured":"Omega. Omega. http:\/\/www.cs.umd.edu\/projects\/omega ."},{"key":"9004_CR31","doi-asserted-by":"crossref","unstructured":"Parthasarathy, G., Iyer, M., Cheng, K.-T. and Wang, L.-C.: An efficient finite-domain constraint solver for circuits, in Proc. DAC'04, 2004, pp. 212\u2013217.","DOI":"10.1145\/996566.996628"},{"key":"9004_CR32","unstructured":"SAL. SAL Suite. http:\/\/www.csl.sri.com\/users\/demoura\/gdp-benchmark.html ."},{"issue":"2\/3","key":"9004_CR33","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E-A Brainiac theorem prover, AI Commun. 15(2\/3) (2002), 111\u2013126.","journal-title":"AI Commun."},{"key":"9004_CR34","unstructured":"SEP. SEP Suite, http:\/\/iew3.technion.ac.il\/~ofers\/smtlib-local\/benchmarks.html ."},{"key":"9004_CR35","doi-asserted-by":"crossref","unstructured":"Seshia, S., Lahiri, S. and Bryant, R.: A hybrid SAT-based decision procedure for separation logic with uninterpreted function, in Proc. DAC'03, pp. 425\u2013430.","DOI":"10.1145\/775832.775945"},{"key":"9004_CR36","unstructured":"Shin, J.-A. and Davis, E.: Continuous time in a SAT-based planner, in Proc. AAAI-04, 2004, pp. 531\u2013536."},{"key":"9004_CR37","unstructured":"Silva, J. P. M. and Sakallah, K. A.: GRASP \u2013 A new search algorithm for satisfiability, in Proc. ICCAD'96, 1996, pp. 220\u2013227."},{"issue":"1","key":"9004_CR38","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/S0004-3702(00)00019-9","volume":"120","author":"K. Stergiou","year":"2000","unstructured":"Stergiou, K. and Koubarakis, M.: Backtracking algorithms for disjunctions of temporal constraints, Artif. Intell. 120(1) (2000), 81\u2013117.","journal-title":"Artif. Intell."},{"key":"9004_CR39","doi-asserted-by":"crossref","unstructured":"Strichman, O.: On solving presburger and linear arithmetic with SAT, in Proc. of Formal Methods in Computer-Aided Design (FMCAD 2002), 2002.","DOI":"10.1007\/3-540-36126-X_10"},{"key":"9004_CR40","unstructured":"Strichman, O., Seshia, S., Bryant, R.: Deciding separation formulas with SAT, in Proc. of Computer Aided Verification, (CAV'02)."},{"key":"9004_CR41","unstructured":"TM. TM-LPSAT. http:\/\/csl.cs.nyu.edu\/~jiae\/ ."},{"key":"9004_CR42","unstructured":"TSAT. TSAT++. http:\/\/www.ai.dist.unige.it\/Tsat ."},{"key":"9004_CR43","unstructured":"UCLID.UCLID. http:\/\/www-2.cs.cmu.edu\/~uclid ."},{"key":"9004_CR44","doi-asserted-by":"crossref","unstructured":"Zhang, L. and Malik, S.: The quest for efficient boolean satisfiability solves, in Proc. CAV'02, 2002, pp. 17\u201336.","DOI":"10.1007\/3-540-45657-0_2"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9004-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-9004-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9004-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T12:05:09Z","timestamp":1586606709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-9004-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10]]},"references-count":44,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2005,10]]}},"alternative-id":["9004"],"URL":"https:\/\/doi.org\/10.1007\/s10817-005-9004-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,10]]}}}