{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,28]],"date-time":"2026-06-28T04:51:57Z","timestamp":1782622317648,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540253334","type":"print"},{"value":"9783540319801","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_21","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T18:44:59Z","timestamp":1278873899000},"page":"317-333","source":"Crossref","is-referenced-by-count":34,"title":["An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic"],"prefix":"10.1007","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","reference":[{"key":"21_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North Holland Pub. Co, Amsterdam (1954)"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Proc. European Conference on Planning, CP 1999 (1999)","DOI":"10.1007\/10720246_8"},{"key":"21_CR3","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":"21_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","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.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 195. Springer, Heidelberg (2002)"},{"key":"21_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-45470-5_22","volume-title":"Artificial Intelligence, Automated Reasoning, and Symbolic Computation","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Korni\u0142owicz, A., Sebastiani, R.: Integrating boolean and mathematical solving: Foundations, basic algorithms and requirements. In: Calmet, J., Benhamou, B., Caprotti, O., H\u00e9nocque, L., Sorge, V. (eds.) AISC 2002 and Calculemus 2002. LNCS (LNAI), vol.\u00a02385, pp. 231\u2013245. Springer, Heidelberg (2002)"},{"key":"21_CR6","unstructured":"Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying Industrial Hybrid Systems with MathSAT. In: Proc. of the 1st CADE-19 Workshop on Pragmatics of Decision Procedures in Automated Reasoning, PDPAR 2003 (2003)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_16","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Cimatti, A., Korni\u0142owicz, A., Sebastiani, R.: SAT-Based Bounded Model Checking for Timed Systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, Springer, Heidelberg (2002)"},{"key":"21_CR8","unstructured":"Badros, G.J., Borning, A.: The Cassowary linear arithmetic constraint solving algorithm: Interface and implementation. Technical Report UW-CSE-98-06-04 (Jun 1998)"},{"key":"21_CR9","first-page":"457","volume-title":"Proc. CAV 2004","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 2004, pp. 457\u2013461. Springer, Heidelberg (2004)"},{"key":"21_CR10","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. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"21_CR11","first-page":"203","volume-title":"Proc. AAAI\/IAAI 1997","author":"R.J. Bayardo Jr.","year":"1997","unstructured":"Bayardo Jr., R.J., Schrag, R.C.: Using CSP Look-Back Techniques to Solve Real-World SAT instances. In: Proc. AAAI\/IAAI 1997, pp. 203\u2013208. AAAI Press, Menlo Park (1997)"},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1016\/B978-044450813-3\/50014-X","volume-title":"Handbook of Automated Reasoning","author":"A. Bockmayr","year":"2001","unstructured":"Bockmayr, A., Weispfenning, V.: Solving Numerical Constraints. In: Handbook of Automated Reasoning, pp. 751\u2013842. MIT Press, Cambridge (2001)"},{"key":"21_CR13","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/263407.263518","volume-title":"Proc. UIST 1997","author":"A. Borning","year":"1997","unstructured":"Borning, A., Marriott, K., Stuckey, P., Xiao, Y.: Solving linear arithmetic constraints for user interface applications. In: Proc. UIST 1997, pp. 87\u201396. ACM, New York (1997)"},{"key":"21_CR14","unstructured":"Bozzano, M., Cimatti, A., Colombini, G., Kirov, V., Sebastiani, R.: The MathSat solver \u2013 a progress report. In: Proc. Workhop on Pragmatics of Decision Procedures in Automated Reasoning 2004, PDPAR 2004 (2004)"},{"key":"21_CR15","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, Los Alamitos (2002)"},{"issue":"2","key":"21_CR16","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s101070050058","volume":"85","author":"B.V. Cherkassky","year":"1999","unstructured":"Cherkassky, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. Mathematical Programming\u00a085(2), 277\u2013311 (1999)","journal-title":"Mathematical Programming"},{"key":"21_CR17","unstructured":"CVC, CVCLite and SVC, http:\/\/verify.stanford.edu\/CVC,CVCL,SVC"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing (SAT 2003)","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"21_CR19","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., Ruess, 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":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","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, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"21_CR21","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)"},{"key":"21_CR22","unstructured":"Gomes, C., Selman, B., Kautz, H.: Boosting Combinatorial Search Through Randomization. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence (1998)"},{"key":"21_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/3-540-69778-0_5","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"I. Horrocks","year":"1998","unstructured":"Horrocks, I., Patel-Schneider, P.F.: FaCT and DLP. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 27\u201330. Springer, Heidelberg (1998)"},{"key":"21_CR24","unstructured":"ICS, http:\/\/www.icansolve.com"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-Based Satisfiability Solving of Presburger Arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"key":"21_CR26","unstructured":"mathsat, http:\/\/mathsat.itc.it"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhang, Y.Z.L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (2001)","DOI":"10.1145\/378239.379017"},{"key":"21_CR28","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-39813-4_5","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 (LNAI), vol.\u00a02850, pp. 77\u201389. Springer, Heidelberg (2003)"},{"key":"21_CR29","unstructured":"Omega, http:\/\/www.cs.umd.edu\/projects\/omega"},{"key":"21_CR30","first-page":"212","volume-title":"Proc. DAC 2004","author":"G. Parthasarathy","year":"2004","unstructured":"Parthasarathy, G., Iyer, M.K., Cheng, K.-T.: An efficient finite-domain constraint solver for circuits. In: Proc. DAC 2004, pp. 212\u2013217. IEEE, Los Alamitos (2004)"},{"key":"21_CR31","unstructured":"SAL Suite. http:\/\/www.csl.sri.com\/users\/demoura\/gdp-benchmarks.html"},{"issue":"2\/3","key":"21_CR32","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"AI Communications"},{"key":"21_CR33","first-page":"425","volume-title":"Proc. DAC 2003","author":"S.A. Seshia","year":"2003","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proc. DAC 2003, pp. 425\u2013430. ACM, New York (2003)"},{"key":"21_CR34","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - A new Search Algorithm for Satisfiability. In: Proc. ICCAD 1996 (1996)"},{"key":"21_CR35","unstructured":"TSAT, http:\/\/www.ai.dist.unige.it\/Tsat"},{"key":"21_CR36","unstructured":"UCLID, http:\/\/www-2.cs.cmu.edu\/~uclid"},{"key":"21_CR37","unstructured":"Wolfman, S., Weld, D.: The LPSAT Engine & its Application to Resource Planning. In: Proc. IJCAI (1999)"},{"key":"21_CR38","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","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31980-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:25:47Z","timestamp":1559244347000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}