{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:03:33Z","timestamp":1725483813407},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441205"},{"type":"electronic","value":"9783540461357"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46135-3_78","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T01:59:47Z","timestamp":1179194387000},"page":"783-783","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Generation of Implied Clauses for SAT"],"prefix":"10.1007","author":[{"given":"Lyndon","family":"Drake","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Frisch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toby","family":"Walsh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"78_CR1","doi-asserted-by":"crossref","unstructured":"S. A. Cook. The complexity of theorem-proving procedures. In Proceedings of the Third ACM Symposium on Theory of Computing, pages 151\u2013158, 1971.","DOI":"10.1145\/800157.805047"},{"key":"78_CR2","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5:394\u2013397, 1962.","journal-title":"Communications of the ACM"},{"key":"78_CR3","unstructured":"Jo\u00e3o P. Marques Silva and Karem A. Sakallah. Conflict analysis in search algorithms for satisfiability. In Proceedings of the IEEE International Conference on Tools with Artificial Intelligence, Nov 1996."},{"key":"78_CR4","unstructured":"Irina Rish and Rina Dechter. Resolution versus search: Two strategies for SAT. In Ian Gent, Hans van Maaren, and Toby Walsh, editors, SAT2000: Highlights of Satisfiability Research in the Year 2000, volume 63 of Frontiers in Artificial Intelligence and Applications, pages 215\u2013259. IOS Press, 2000."},{"key":"78_CR5","doi-asserted-by":"crossref","unstructured":"Allen van Gelder. Satisfiability testing with more reasoning and less guessing. In D. S. Johnson and M. Trick, editors, Cliques, Coloring, and Satisfiability: Second DIM ACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1995.","DOI":"10.1090\/dimacs\/026\/27"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming - CP 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46135-3_78","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:25:15Z","timestamp":1556396715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46135-3_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441205","9783540461357"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/3-540-46135-3_78","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2002]]}}}