{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:37:45Z","timestamp":1725493065242},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_26","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T21:02:07Z","timestamp":1193432527000},"page":"347-363","source":"Crossref","is-referenced-by-count":18,"title":["Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability"],"prefix":"10.1007","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Massimo","family":"Maratea","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]},{"given":"Davide","family":"Zambonin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"key":"26_CR1","unstructured":"J. Gu, P. W. Purdom, J. Franco, and B. W. Wah. Algorithms for the satisfiability (sat) problem: A survey. In Satisfiability Problem: Theory and Applications, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 19\u2013153. AMS, 1997."},{"key":"26_CR2","unstructured":"D. G. Mitchell, B. Selman, and H. J. Levesque. Hard and Easy Distributions for SAT Problems. In Proc. of AAAI, pages 459\u2013465. AAAI Press, 1992."},{"key":"26_CR3","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","volume":"5","author":"J. Franco","year":"1983","unstructured":"J. Franco and M. Paull. Probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem. Discrete Applied Mathematics, 5:77\u201387, 1983.","journal-title":"Discrete Applied Mathematics"},{"key":"26_CR4","unstructured":"Bart Selman, Henry Kautz, and David McAllester. Ten Challenges in Propositional Reasoning and Search. In Proc. of IJCAI, pages 50\u201354. Morgan-Kauffmann, 1997."},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Massacci and Marraro. Logical Cryptanalysis as a SAT Problem. JAR: Journal of Automated Reasoning, 24, 2000.","DOI":"10.1023\/A:1006155811656"},{"key":"26_CR6","unstructured":"Chu Min Li. Integrating Equivalency Reasoning into Davis-Putnam Procedure. In Proc. of AAAI. AAAI Press, 2000."},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"T. E. Uribe and M. E. Stickel. Ordered Binary Decision Diagrams and the Davis-Putnam Procedure. In Proc. of the 1st International Conference on Constraints in Computational Logics, 1994.","DOI":"10.1007\/BFb0016843"},{"key":"26_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Proceedings of TACAS","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. In Proceedings of TACAS, volume 1579 of LNCS, pages 193\u2013207. Springer Verlag, 1999."},{"key":"26_CR9","unstructured":"H. Zhang and M. E. Stickel. Implementing the Davis-Putnam Method. In Highlights of Satisfiability Research in the Year 2000."},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"R. J. Bayardo, Jr. and R. C. Schrag. Using CSP Look-Back Techniques to Solve Real-World SAT instances. In Proc. of AAAI, pages 203\u2013208. AAAI Press, 1997.","DOI":"10.1007\/3-540-61551-2_65"},{"key":"26_CR11","unstructured":"Chu Min Li and Anbulagan. Heuristics Based on Unit Propagation for Satisfiability Problems. In Proc. of IJCAI, pages 366\u2013371. Morgan-Kauffmann, 1997."},{"key":"26_CR12","unstructured":"Jon W. Freeman. Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania, 1995."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An efficient propositional prover. In Proc. of CADE, volume 1249 of LNAI, pages 272\u2013275. Springer Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_28"},{"issue":"7","key":"26_CR14","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7):394\u2013397, 1962.","journal-title":"Journal of the ACM"},{"key":"26_CR15","unstructured":"T. H. Cormen, C. E. Leiserson, and R. R. Rivest. Introduction to Algorithms. MIT Press, 1998."},{"issue":"1-2","key":"26_CR16","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/S0004-3702(99)00097-1","volume":"116","author":"P. Liberatore","year":"2000","unstructured":"P. Liberatore. On the complexity of choosing the branching literal in DPLL. Artificial Intelligence, 116(1-2):315\u2013326, 2000.","journal-title":"Artificial Intelligence"},{"key":"26_CR17","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0004-3702(91)90006-6","volume":"49","author":"R. Dechter","year":"1991","unstructured":"R. Dechter, I. Meiri, and J. Pearl. Temporal Constraint Networks. Artificial Intelligence, 49:61\u201395, 1991.","journal-title":"Artificial Intelligence"},{"key":"26_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CAV","author":"F. Copty","year":"2001","unstructured":"F. Copty, L. Fix, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi. Benefits of Bounded Model Checking at an Industrial Setting. In Proc. of CAV, LNCS. Springer Verlag, 2001. To appear."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T01:51:16Z","timestamp":1556934676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}