{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:37:45Z","timestamp":1725521865187},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540410447"},{"type":"electronic","value":"9783540453314"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-45331-8_25","type":"book-chapter","created":{"date-parts":[[2008,11,27]],"date-time":"2008-11-27T19:39:26Z","timestamp":1227814766000},"page":"261-271","source":"Crossref","is-referenced-by-count":0,"title":["Complexity Issues in the Davis and Putnam Scheme"],"prefix":"10.1007","author":[{"given":"G.","family":"Escalada-Imaz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Torres Vel\u00e1zquez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"G. Ausiello and G. F. Italiano. Online algorithms for poly normally solvable satisfiability problems. Journal of Logic Programming, 10(1), 1991.","DOI":"10.1016\/0743-1066(91)90006-B"},{"key":"25_CR2","unstructured":"C.M. Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the 15th IJCAI, pages 366\u2013371, 1997."},{"key":"25_CR3","unstructured":"J.M. Crawford and L. D. Auton. Experimental results on the crossover point in satisfiability problems. In Proc. of the Eleventh National Conference on Artificial Intelligence, AAAI-93, pages 21\u201327, 1993."},{"key":"25_CR4","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. Comunnications of the ACM, 5:394\u2013397, 1962.","journal-title":"Comunnications of the ACM"},{"key":"25_CR5","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:394\u2013397, 1960.","journal-title":"Journal of the ACM"},{"key":"25_CR6","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1023\/A:1018924526592","volume":"23","author":"G. Davydov","year":"1998","unstructured":"G. Davydov, I. Davydova, and H. K. Buning. An efficient algorithm for the minimal unsatisfiability problem for a classe of cnf. Annals of Mathematics and Artificial Intelligence, 23:229\u2013245, 1998.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"R. Dechter and I. Rish. Rirectional resolution: the davis and putnam procedure revisited. In Proceedings of Knowledge Representattion International Conference, KR-94, pages 134\u2013145, 1994.","DOI":"10.1016\/B978-1-4832-1452-8.50109-3"},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"3","author":"W.F. Dowling","year":"1984","unstructured":"W.F. Dowling and J. H. Gallier. Linear-time algorithms for testing the satisfiability of horn prepositional formulae. Journal of Logic Programming, 3:267\u2013284, 1984.","journal-title":"Journal of Logic Programming"},{"key":"25_CR9","unstructured":"D. Dubois, P. Andre, Y. Boufkhad, and J. Carlier. Sat versus unsat. In Proceedings of the Second DIM ACS Challenge, 1993."},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/0304-3975(77)90054-8","volume":"4","author":"Z. Galil","year":"1977","unstructured":"Z. Galil. On the complexity of Regular Resolution and the Davis-Putnam procedure. Theoretical Computer Sicence, 4:23\u201346, 1977.","journal-title":"Theoretical Computer Sicence"},{"key":"25_CR11","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/BF00881805","volume":"15","author":"J.N. Hooker","year":"1995","unstructured":"J.N. Hooker and V. Vinay. Branching rules for satisfiability. Journal of Automated Reasoning, 15:359\u2013383, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0004-3702(95)00046-1","volume":"81","author":"J.M. Crawford","year":"1996","unstructured":"J.M. Crawford and L. D. Auton. Experimental Results on the Crossover Point in random 3-SAT. Artificial Intelligence, 81:31\u201357, 1996.","journal-title":"Artificial Intelligence"},{"key":"25_CR13","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R.E. Jeroslow","year":"1990","unstructured":"R.E. Jeroslow and J. Wang. Solving prepositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167\u2013187, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"25_CR14","unstructured":"H. Kautz and B. Selman. Planing as satisfiability. In Proceeding of the 10th EC AI, pages 359\u2013363. European Conference on Artificial Intelligence, 1992."},{"key":"25_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/3-540-60299-2_31","volume-title":"Principles and Practice of Constraint Programming, CP\u201995","author":"A. Rauzy","year":"1995","unstructured":"A. Rauzy. Polynomial restrictions of sat: What ca be done with an efficient implementation of the davis and putnam\u2019s procedure. In U. Mntanari and F. Rossi, editors, Principles and Practice of Constraint Programming, CP\u201995, volume 976 of Lecture Notes in Computer Science, pages 515\u2013532. Fisrt International Conference on Principles and Practice of Constraint Programming, Cassis, France, Springer-verlag, 1995."},{"key":"25_CR16","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1137\/0606031","volume":"6","author":"T.E. Tarjan","year":"1985","unstructured":"T.E. Tarjan. Amortized computational complexity. SIAM J. Algebraic Discrete Methods, 6:306\u2013318, 1985.","journal-title":"SIAM J. Algebraic Discrete Methods"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"H. Zhang. Sato: An efficient prepositional prover. In proceedings of the 13th Conference on Automated Deduction, pages 272\u2013275, 1997.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"25_CR18","unstructured":"H. Zhang and M. E. Stickel. An efficient algorithm for unit propagation. In International Symposium on Artificial Intelligence and Mathematics, 1996."},{"key":"25_CR19","unstructured":"H Zhang and M. E. Stickel. Implementing the davis-putnam algorithm by tries. Technical report, The University of Iowa, 1994."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence: Methodology, Systems, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45331-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T16:29:52Z","timestamp":1557937792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45331-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410447","9783540453314"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45331-8_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}