{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:15Z","timestamp":1776333495766,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540438656","type":"print"},{"value":"9783540454700","type":"electronic"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45470-5_22","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T06:38:36Z","timestamp":1186900716000},"page":"231-245","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Audemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piergiorgio","family":"Bertoli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"Korni\u0142owicz","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":[[2002,6,21]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"[ABC+02]_G. Audemard, P. Bertoli, A. Cimatti, A. Korni\u0142owicz, and R. Sebastiani. A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In Proc. CADE\u20192002., 2002. To appear. Available at \n                    http:\/\/www.dit.unitn.it\/~rseba\/publist.html\n                    \n                  .","DOI":"10.1007\/3-540-45620-1_17"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"A. Armando, C. Castellini, and E. Giunchiglia. SAT-based procedures for temporal reasoning. In Proc. European Conference on Planning, CP-99, 1999.","DOI":"10.1007\/10720246_8"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"G. Audemard, A. Cimatti, A. Korni\u0142owicz, and R. Sebastiani. SAT-Based Bounded Model Checking for Timed Systems. 2002. Available at \n                    http:\/\/www.dit.unitn.it\/~rseba\/publist.html\n                    \n                  .","DOI":"10.1007\/3-540-36135-9_16"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. CAV\u201999, 1999.","DOI":"10.21236\/ADA360973"},{"issue":"8","key":"22_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"22_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-63166-6_32","volume-title":"Proc. CAV\u201997","author":"W. Chan","year":"1997","unstructured":"W. Chan, R. J. Anderson, P. Beame, and D. Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In Proc. CAV\u201997, volume 1254 of LNCS, pages 316\u2013327, Haifa, Israel, June 1997. Springer-Verlag."},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.","DOI":"10.1145\/368273.368557"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K. In Proc. of the 13th Conference on Automated Deduction, LNAI, New Brunswick, NJ, USA, August 1996. Springer Verlag.","DOI":"10.1007\/3-540-61511-3_115"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K(m). Information and Computation, 162(1\/2), October\/November 2000.","DOI":"10.1006\/inco.1999.2850"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"I. Horrocks and P. F. Patel-Schneider. FaCT and DLP. In Procs. Tableaux\u201998, number 1397 in LNAI, pages 27\u201330. Springer-Verlag, 1998.","DOI":"10.1007\/3-540-69778-0_5"},{"key":"22_CR11","unstructured":"H. Kautz, D. McAllester, and Bart Selman. Encoding Plans in Propositional Logic. In Proc. KR\u201996, 1996."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"J. Moeller, J. Lichtenberg, H. Andersen, and H. Hulgaard. Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams. In Electronic Notes in Theoretical Computer Science, volume 23. Elsevier Science, 2001.","DOI":"10.1016\/S1571-0661(04)80671-6"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"W. Pugh. The Omega Test: a fast and practical integer programming algoprithm for dependence analysis. Communication of the ACM, August 1992.","DOI":"10.1145\/125826.125848"},{"key":"22_CR14","unstructured":"A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science Publishers, 2001."},{"key":"22_CR15","unstructured":"R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001. Available at \n                    http:\/\/www.dit.unitn.it\/~rseba\/publist.html\n                    \n                  ."},{"key":"22_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R. M. Smullyan","year":"1968","unstructured":"R. M. Smullyan. First-Order Logic. Springer-Verlag, NY, 1968."},{"key":"22_CR17","unstructured":"S. Wolfman and D. Weld. The LPSAT Engine & its Application to Resource Planning. In Proc. IJCAI, 1999."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence, Automated Reasoning, and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45470-5_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T14:23:38Z","timestamp":1558275818000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45470-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540438656","9783540454700"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45470-5_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"21 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}