{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:45:09Z","timestamp":1725486309488},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441274"},{"type":"electronic","value":"9783540461487"}],"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-46148-5_6","type":"book-chapter","created":{"date-parts":[[2007,6,7]],"date-time":"2007-06-07T02:31:45Z","timestamp":1181183505000},"page":"51-60","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Using Failed Local Search for SAT as an Oracle for Tackling Harder A.I. Problems More Efficiently"],"prefix":"10.1007","author":[{"given":"\u00c9ric","family":"Gr\u00e9goire","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Mazure","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lakhdar","family":"Sais","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,8,21]]},"reference":[{"key":"6_CR1","unstructured":"S. Benferhat, C. Cayrol, D. Dubois, J. Lang, and H. Prade. Inconsistency management and prioritized syntax-based entailment. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI\u201993), pages 640\u2013645, 1993."},{"key":"6_CR2","unstructured":"Yacine Boufkhad and Olivier Roussel. Redundancy in random sat formulas. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI\u201900), pages 273\u2013278, 2000."},{"key":"6_CR3","unstructured":"James M. Crawford. Solving satisfiability problems using a combination of systematic and local search. In Working notes of the DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability, 1993."},{"key":"6_CR4","doi-asserted-by":"crossref","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. Journal of the Association for Computing Machinery, 5:394\u2013397, 1962.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"6_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/3-540-48747-6_16","volume-title":"Handling inconsistency efficiently in the incremental construction of stratified belief bases","author":"\u00c9. Gr\u00e9goire","year":"1999","unstructured":"\u00c9ric Gr\u00e9goire. Handling inconsistency efficiently in the incremental construction of stratified belief bases. In A. Hunter and S. Parsons, editors, Proceedings of the Fifth European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty (ECSQARU\u201999), volume 1638 of Lecture Notes in Computer Science, pages 168\u2013178, London (UK), July 1999. Springer."},{"issue":"2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1142\/S0218213000000082","volume":"9","author":"\u00c9. Gr\u00e9goire","year":"2000","unstructured":"\u00c9ric Gr\u00e9goire and David Ansart. Overcoming the christmas tree syndrome. International Journal on Artificial Aintelligence Tools (IJAIT), 9(2):97\u2013111, 2000.","journal-title":"International Journal on Artificial Aintelligence Tools (IJAIT)"},{"key":"6_CR7","unstructured":"W. Hamscher, L. Console, and J. De Kleer. Readings in Model-Based Diagnosis. Morgan Kaufmann, 1992."},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/BF02241270","volume":"22","author":"P. Hansen","year":"1990","unstructured":"Pierre Hansen and Brigitte Jaumard. Algorithms for the maximum satisfiability problem. Journal of Computing, 22:279\u2013303, 1990.","journal-title":"Journal of Computing"},{"key":"6_CR9","unstructured":"Bertrand Mazure. De la Satisfaisabilit\u00e9 \u00e0 la Compilation de Bases de Connaissances Propositionnelles. Th\u00e8se de doctorat, Universit\u00e9 d\u2019Artois, Centre de Recherche en Informatique de Lens (Facult\u00e9 Jean Perrin), January 1999."},{"key":"6_CR10","unstructured":"Bertrand Mazure, Lakhdar Sais, and \u00c9ric Gr\u00e9goire. Tabu search for SAT. In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI'97), pages 281\u2013285, Providence (Rhode Island, USA), July 1997."},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1018999721141","volume":"22","author":"B. Mazure","year":"1998","unstructured":"Bertrand Mazure, Lakhdar Sais, and \u00c9ric Gr\u00e9goire. Boosting complete techniques thanks to local search methods. Annals of Mathematics and Artificial Intelligence, 22:319\u2013331, 1998.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Bertrand Mazure, Lakhdar Sais, and \u00c9ric Gr\u00e9goire. System Description: CRIL Platform for SAT. In Proceedings of the Fifteenth International Conference on Automated Deduction (CADE\u201915), volume 1421 of Lecture Notes in Artificial Intelligence, pages 116\u2013119, Lindau (Germany), July 1998.","DOI":"10.1007\/BFb0054253"},{"key":"6_CR13","unstructured":"David A. McAllester, Bart Selman, and Henry A. Kautz. Evidence for invariants in local search. In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI\u201997), pages 321\u2013326, August 1997."},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/0004-3702(86)90032-9","volume":"28","author":"J. McCarthy","year":"1986","unstructured":"J. McCarthy. Applications of circumscription to formalizing common-sense knowledge. Artificial Intelligence, 28:89\u2013116, 1986.","journal-title":"Artificial Intelligence"},{"key":"6_CR15","unstructured":"P. Morris. The break out method for escaping from local minima. In Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI\u201993), pages 40\u201345, 1993."},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R. Reiter","year":"1987","unstructured":"R. Reiter. A theory of diagnosis from first principles. Artificial Intelligence, 32:57\u201395, 1987.","journal-title":"Artificial Intelligence"},{"key":"6_CR17","unstructured":"Bart Selman, Henry A. Kautz, and B. Cohen. Local search strategies for satisfiability testing. In Working notes of the DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability, 1993."},{"key":"6_CR18","unstructured":"Bart Selman, Hector J. Levesque, and David Mitchell. Gsat: A new method for solving hard satisfiability problems. In Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI\u201992), pages 440\u2013446, 1992."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence: Methodology, Systems, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46148-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:48:55Z","timestamp":1558273735000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46148-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441274","9783540461487"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-46148-5_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"21 August 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}