{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T14:25:04Z","timestamp":1747578304208,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540428633"},{"type":"electronic","value":"9783540455783"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1007\/3-540-45578-7_48","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T06:34:25Z","timestamp":1180334065000},"page":"605-609","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Solving Boolean Satisfiability Using Local Search Guided by Unit Clause Elimination"],"prefix":"10.1007","author":[{"given":"Edward A.","family":"Hirsch","sequence":"first","affiliation":[]},{"given":"Arist","family":"Kojevnikov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,11,19]]},"reference":[{"key":"48_CR1","unstructured":"E. Dantsin, E.A. Hirsch, S. Ivanov,and M. Vsemirnov. Algorithms for SAT and upper bounds on their complexity.ECCC Technical Report 01-012, ftp:\/\/ftp.eccc.unitrier.de\/pub\/eccc\/reports\/2001\/TR01-012\/index.html ."},{"key":"48_CR2","doi-asserted-by":"crossref","unstructured":"J. Gu, P.W. Purdom, J. Franco, and B.W. Wah. Algorithms for satisfiability (SAT)problem:A survey.DIMACS Ser.in DM and TCS 35,1997,pages 19\u2013152.","DOI":"10.1090\/dimacs\/035\/02"},{"key":"48_CR3","unstructured":"H.H. Hoos.On the run-time behaviour of stochastic local search algorithms for SAT. In Proc.AAAI\u201999,pages 661\u2013666."},{"key":"48_CR4","unstructured":"H.H. Hoos. Stochastic Local Search-Method,Models,Applications.PhD thesis, Department of Computer Science, Darmstadt University of Technology,1998."},{"key":"48_CR5","unstructured":"H.H. Hoos and T. St\u00fctzle. SATLIB. http:\/\/www.satlib.org\/ ."},{"issue":"4","key":"48_CR6","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1023\/A:1006350622830","volume":"24","author":"H.H. Hoos","year":"2000","unstructured":"H.H. Hoos and T. St\u00fctzle. Local search algorithms for SAT:An empirical evaluation. Journal of Automated Reasoning,24(4):421\u2013481,2000.","journal-title":"Journal of Automated Reasoning"},{"key":"48_CR7","doi-asserted-by":"crossref","unstructured":"D.S. Johnson and M.A. Tricks,editors. Cliques,Coloring and Satisfiability, volume 26 of DIMACS Ser.in DM and TCS.AMS,1996.","DOI":"10.1090\/dimacs\/026"},{"key":"48_CR8","unstructured":"D. McAllester, B. Selman,and H. Kautz. Evidence in invariants for local search. In Proc.AAAI\u201997,pages 321\u2013326."},{"key":"48_CR9","doi-asserted-by":"crossref","unstructured":"R. Paturi, P. Pudl \u00e1k, M.E. Saks,and F. Zane. An improved exponential-time algorithm for k-SAT. In Proc.FOCS\u201998,pages 628\u2013637.","DOI":"10.1109\/SFCS.1998.743513"},{"key":"48_CR10","unstructured":"S.D. Prestwich. Local search and backtracking vs non-systematic backtracking. In AAAI 2001 Fall Symposium on Using Uncertainty within Computation.To appear."},{"key":"48_CR11","doi-asserted-by":"crossref","unstructured":"U. Sch\u00f6ning. A probabilistic algorithm for k-SAT and constraint satisfaction problems. InProc.FOCS\u201999,pages 410\u2013414.","DOI":"10.1109\/SFFCS.1999.814612"},{"key":"48_CR12","unstructured":"R. Schuler, U. Sch\u00f6ning,and O. Watanabe. An improved randomized algorithm for 3-SAT. Technical Report TR-C146, Dept.of Math.and Comp.Sci.,Tokyo Inst.of Tech.,2001."},{"key":"48_CR13","unstructured":"D. Schuurmans and F. Southey. Local search characteristics of incomplete SAT procedures. In Proc.of AAAI\u20192000,pages 297\u2013302."},{"key":"48_CR14","unstructured":"B. Selman, H. A. Kautz, and B. Cohen. Noise strategies for improving local search. In Proc.AAAI\u201994,pages 337\u2013343."},{"key":"48_CR15","unstructured":"B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In Proc.AAAI\u201992,pages 440\u2013446."}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2014 CP 2001"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45578-7_48","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:36:41Z","timestamp":1737052601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45578-7_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540428633","9783540455783"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45578-7_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"19 November 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}