{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:18:51Z","timestamp":1775053131105,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540673507","type":"print"},{"value":"9783540462385","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46238-4_8","type":"book-chapter","created":{"date-parts":[[2007,7,31]],"date-time":"2007-07-31T22:05:23Z","timestamp":1185919523000},"page":"84-94","source":"Crossref","is-referenced-by-count":18,"title":["Applying the Davis-Putnam procedure to non-clausal formulas"],"prefix":"10.1007","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"issue":"3\u20134","key":"8_CR1","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/BF01530803","volume":"8","author":"A. Armando","year":"1993","unstructured":"A. Armando and E. Giunchiglia. Embedding Complex Decision Procedures inside an Interactive Theorem Prover. Annals of Mathematics and Artificial Intelligence, 8(3\u20134):475\u2013502, 1993.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"12","key":"8_CR2","volume":"81","year":"1996","unstructured":"Artificial Intelligence, 81(1,2), 1996. Special Volume on Frontiers in Probelm Solving: Phase Transitions and Complexity.","journal-title":"Artificial Intelligence"},{"issue":"8","key":"8_CR3","doi-asserted-by":"publisher","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":"8_CR4","doi-asserted-by":"crossref","unstructured":"J. Crawford and L. Auton. Experimental results on the crossover point in 3SAT. Artificial Intelligence, 81, 1996.","DOI":"10.1016\/0004-3702(95)00046-1"},{"issue":"3","key":"8_CR5","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M. D\u2019Agostino","year":"1994","unstructured":"M. D\u2019Agostino and M. Mondadori. The Taming of the Cut. Journal of Logic and Computation, 4(3):285\u2013319, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"8_CR6","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":"8_CR7","doi-asserted-by":"publisher","first-page":"201","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:201\u2013215, 1960.","journal-title":"Journal of the ACM"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour. Minimizing the Number of Clauses by Renaming. In Proc. CADE-90, pages 558\u2013572. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_114"},{"key":"8_CR9","volume-title":"The Second DIMACS International Algorithm Implementation Challenge","author":"DIMACS.","year":"1993","unstructured":"DIMACS. The Second DIMACS International Algorithm Implementation Challenge, Rutgers University, USA, 1993."},{"key":"8_CR10","unstructured":"E. Giunchiglia, F. Giunchiglia, R. Sebastiani, and A. Tacchella. More evaluation of decision procedures for modal logics. In Proc. KR\u201998, 1998."},{"key":"8_CR11","unstructured":"E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act, and the rest will follow: Exploiting determinism in planning as satisfiability. In Proc. AAAI-98, 1998."},{"key":"8_CR12","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. CADE-96, Lecture Notes in Artificial Intelligence. Springer Verlag.","DOI":"10.1007\/3-540-61511-3_115"},{"key":"8_CR13","unstructured":"F. Giunchiglia and R. Sebastiani. A SAT-based decision procedure for ALC. In Proc. KR\u201996, Cambridge, MA, USA, November 1996."},{"key":"8_CR14","unstructured":"Henry Kautz, David McAllester, and Bart Selman. Exploiting variable dependency in local search. In Abstracts of the Poster Sessions of IJCAI-97, August 23\u201329 1997. Available at http:\/\/www.research.att.com\/~kautz\/papers-ftp\/index.html ."},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"D.A. Plaisted and S. Greenbaum. A Structure-preserving Clause Form Translation. Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR16","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1613\/jair.49","volume":"1","author":"R. Sebastiani","year":"1994","unstructured":"R. Sebastiani. Applying GSAT to Non-Clausal Formulas. Journal of Artificial Intelligence Research, 1:309\u2013314, 1994.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"8_CR17","unstructured":"B. Selman, H. Levesque., and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proc. AAAI-92, pages 440\u2013446, 1992."},{"key":"8_CR18","unstructured":"Bart Selman, Henry A. Kautz, and Bram Cohen. Noise strategies for improving local search. In Proc. AAAI-94, pages 337\u2013343. AAAI Press."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"J\u00f6rg Siekmann and Graham Wrightson, editors. Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, volume 2. Springer-Verlag, 1983.","DOI":"10.1007\/978-3-642-81952-0"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"G. Tseitin. On the complexity of proofs in propositional logics. Seminars in Mathematics, 8, 1970. Reprinted in [19].","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"8_CR21","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":"8_CR22","unstructured":"H. Zhang and M. Stickel. Implementing the Davis-Putnam algorithm by tries. Technical report, University of Iowa, August 1994."}],"container-title":["Lecture Notes in Computer Science","AI*IA 99: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46238-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T12:29:38Z","timestamp":1556713778000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46238-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540673507","9783540462385"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-46238-4_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}