{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:08:01Z","timestamp":1761620881858},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2004,12,31]],"date-time":"2004-12-31T00:00:00Z","timestamp":1104451200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s10472-005-0421-9","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T19:19:42Z","timestamp":1109791182000},"page":"91-111","source":"Crossref","is-referenced-by-count":21,"title":["UnitWalk: A new SAT solver that uses local search guided by unit clause elimination"],"prefix":"10.1007","volume":"43","author":[{"given":"Edward A.","family":"Hirsch","sequence":"first","affiliation":[]},{"given":"Arist","family":"Kojevnikov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,12,31]]},"reference":[{"key":"421_CR1","doi-asserted-by":"crossref","unstructured":"F. Asahiro, K. Iwama and E. Miyano, Random generation of test instances with controlled attributes, in: [17] (1996).","DOI":"10.1090\/dimacs\/026\/18"},{"key":"421_CR2","unstructured":"J. Culberson, I.P. Gent and H.H. Hoos, On the probabilistic approximate completeness of WalkSAT for 2-SAT, Technical Report APES-15A-2000, Department of Computer Science, University of Strathclyde (2000)."},{"key":"421_CR3","first-page":"24","volume":"105","author":"E. Dantsin","year":"1981","unstructured":"E. Dantsin, Two propositional proof systems based on the splitting method, Zapiski Nauchnykh Seminarov LOMI 105 (1981) 24\u201344 (in Russian), English translation: Journal of Soviet Mathematics 22(3) (1983) 1293\u20131305.","journal-title":"Zapiski Nauchnykh Seminarov LOMI"},{"issue":"1","key":"421_CR4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0304-3975(01)00174-8","volume":"289","author":"E. Dantsin","year":"2002","unstructured":"E. Dantsin, A. Goerdt, E.A. Hirsch, R. Kannan, J. Kleinberg, C. Papadimitriou, P. Raghavan and U. Sch\u00f6ning, A deterministic (2 \u2212 2 (k + 1)) n algorithm for k-SAT based on local search, Theoretical Computer Science 289(1) (2002) 69\u201383.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"421_CR5","doi-asserted-by":"crossref","first-page":"4948","DOI":"10.1023\/A:1025645221773","volume":"118","author":"E.Y. Dantsin","year":"2003","unstructured":"E.Y. Dantsin, E.A. Hirsch, S.V. Ivanov and M.V. Vsemirnov, Algorithms for SAT and upper bounds on their complexity, Journal of Mathematical Sciences 118(2) (2003) 4948\u20134962, Russian original appears in: Zapiski Nauchnykh Seminarov POMI 277 (2001) 14\u201346.","journal-title":"Journal of Mathematical Sciences"},{"key":"421_CR6","unstructured":"I.P. Gent and T. Walsh, Towards an understanding of hill-climbing procedures for SAT, in: Proceedings of the 11th National Conference on Artificial Intelligence, AAAI\u201993 (1993) pp. 28\u201333."},{"key":"421_CR7","unstructured":"I.P. Gent and T. Walsh, Unsatisfied variables in local search, in: Hybrid Problems, Hybrid Solutions, ed. J. Hallam (IOS Press, 1995) pp. 73\u201385."},{"issue":"1","key":"421_CR8","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/130836.130837","volume":"3","author":"J. Gu","year":"1992","unstructured":"J. Gu, Efficient local search for very large-scale satisfiability problems, ACM SIGART Bulletin 3(1) (1992) 8\u201312.","journal-title":"ACM SIGART Bulletin"},{"key":"421_CR9","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-58325-4_176","volume":"834","author":"J. Gu","year":"1994","unstructured":"J. Gu and Q.-P. Gu, Average time complexity of the SAT1.2 algorithm, in: Proceedings of the 5th Annual International Symposium on Algorithms and Computation, ISAAC\u201994, Lecture Notes in Computer Science, Vol. 834 (1994) pp. 146\u2013154.","journal-title":"Lecture Notes in Computer Science"},{"key":"421_CR10","doi-asserted-by":"crossref","unstructured":"J. Gu, P.W. Purdom, J. Franco and B.W. Wah, Algorithms for satisfiability (SAT) problem: A survey, in: Satisfiability Problem: Theory and Applications (DIMACS Workshop), eds. D .Du, J. Gu and P.M. Pardalos, March 11\u201313, 1996, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 35 (AMS, 1997) pp. 19\u2013152.","DOI":"10.1090\/dimacs\/035\/02"},{"issue":"1\u20132","key":"421_CR11","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1023\/A:1006318521185","volume":"24","author":"E.A. Hirsch","year":"2000","unstructured":"E.A. Hirsch, SAT local search algorithms: Worst-case study, Journal of Automated Reasoning 24(1\u20132) (2000) 127\u2013143.","journal-title":"Journal of Automated Reasoning"},{"key":"421_CR12","unstructured":"E.A. Hirsch and A. Kojevnikov, UnitWalk: A new SAT solver that uses local search guided by unit clause elimination, PDMI preprint 9\/2001, Steklov Institute of Mathematics at St. Petersburg (2001)."},{"key":"421_CR13","unstructured":"H.H. Hoos, Stochastic local search \u2014 method, models, applications, Ph.D. thesis, Department of Computer Science, Darmstadt University of Technology (1998)."},{"key":"421_CR14","unstructured":"H.H. Hoos, On the run-time behaviour of stochastic local search algorithms for SAT, in: Proceedings of the 16th National Conference on Artificial Intelligence, AAAI\u201999 (1999) pp. 661\u2013666."},{"issue":"4","key":"421_CR15","doi-asserted-by":"crossref","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) (2000) 421\u2013481.","journal-title":"Journal of Automated Reasoning"},{"key":"421_CR16","unstructured":"H.H. Hoos and T. St\u00fctzle, SATLIB: An online resource for research on SAT, in: Highlights of Satisfiability Research in the Year 2000, Frontiers in Artificial Intelligence and Applications, Vol. 63 (IOS Press, 2000) pp. 283\u2013292."},{"key":"421_CR17","unstructured":"D.S. Johnson and M.A. Tricks (eds.), Cliques, Coloring and Satisfiability, DIMACS Series on Discrete Mathematics and Theoretical Computer Science, Vol. 26, AMS (1996)."},{"key":"421_CR18","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/BF01581082","volume":"57","author":"A.P. Kamath","year":"1992","unstructured":"A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan and M.G.C. Resende, A continuous approach to inductive inference, Mathematical Programming 57 (1992) 215\u2013238.","journal-title":"Mathematical Programming"},{"issue":"1","key":"421_CR19","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0020-0190(92)90029-U","volume":"43","author":"E. Koutsoupias","year":"1992","unstructured":"E. Koutsoupias and C.H. Papadimitriou, On the greedy algorithm for satisfiability, Information Processing Letters 43(1) (1992) 53\u201355.","journal-title":"Information Processing Letters"},{"issue":"1","key":"421_CR20","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"T. Larrabee, Test pattern generation using Boolean satisfiability, IEEE Transactions on Computer-Aided Design 11(1) (1992) 6\u201322.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"421_CR21","unstructured":"C.M. Li and Anbulagan, Heuristics based on unit propagation for satisfiability problems, in: Proceedings of the International Joint Conference on Artificial Intelligence (1997) pp. 366\u2013371."},{"key":"421_CR22","unstructured":"H. Luckhardt, Obere Komplexit\u00e4tsschranken f\u00fcr TAUT-Entscheidungen, in: Proceedings of Frege Conference 1984, Schwerin (1984) pp. 331\u2013337."},{"key":"421_CR23","unstructured":"D. McAllester, B. Selman and H. Kautz, Evidence in invariants for local search, in: Proceedings of the 14th National Conference on Artificial Intelligence, AAAI\u201997 (1997) pp. 321\u2013326."},{"key":"421_CR24","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","volume":"10","author":"B. Monien","year":"1985","unstructured":"B. Monien and E. Speckenmeyer, Solving satisfiability in less then 2 n steps, Discrete Applied Mathematics 10 (1985) 287\u2013295.","journal-title":"Discrete Applied Mathematics"},{"key":"421_CR25","doi-asserted-by":"crossref","unstructured":"M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang and S. Malik, Chaff: Engineering an efficient SAT solver, in: Proceedings of the 38th Design Automation Conference (DAC\u201901) (2001) pp. 530\u2013535.","DOI":"10.1145\/378239.379017"},{"key":"421_CR26","doi-asserted-by":"crossref","unstructured":"C.H. Papadimitriou, On selecting a satisfying truth assignment, in: Proceedings of the 32nd Annual IEEE Symposium on Foundations of Computer Science, FOCS\u201991 (1991) pp. 163\u2013169.","DOI":"10.1109\/SFCS.1991.185365"},{"key":"421_CR27","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: Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science, FOCS\u201998 (1998) pp. 628\u2013637.","DOI":"10.1109\/SFCS.1998.743513"},{"key":"421_CR28","doi-asserted-by":"crossref","unstructured":"R. Paturi, P. Pudl\u00e1k and F. Zane, Satisfiability coding lemma, in: Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, FOCS\u201997 (1997) pp. 566\u2013574.","DOI":"10.1109\/SFCS.1997.646146"},{"key":"421_CR29","unstructured":"S.D. Prestwich, Local search and backtracking vs non-systematic backtracking, in: AAAI 2001 Fall Symposium on Using Uncertainty within Computation (2001)."},{"key":"421_CR30","doi-asserted-by":"crossref","unstructured":"U. Sch\u00f6ning, A probabilistic algorithm for k-SAT and constraint satisfaction problems, in: Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science, FOCS\u201999 (1999) pp. 410\u2013414.","DOI":"10.1109\/SFFCS.1999.814612"},{"key":"421_CR31","unstructured":"R. Schuler, U. Sch\u00f6ning and O. Watanabe, An improved randomized algorithm for 3-SAT, Technical Report TR-C146, Department of Mathematical and Computing Sciences, Tokyo Institute of Technics (2001)."},{"key":"421_CR32","unstructured":"D. Schuurmans and F. Southey, Local search characteristics of incomplete SAT procedures, in: Proc. of AAAI\u20192000 (2000) pp. 297\u2013302."},{"key":"421_CR33","unstructured":"B. Selman, H.A. Kautz and B. Cohen, Noise strategies for improving local search, in: Proceedings of the 12th National Conference on Artificial Intelligence, AAAI\u201994 (1994) pp. 337\u2013343."},{"key":"421_CR34","unstructured":"B. Selman, H. Levesque and D. Mitchell, A new method for solving hard satisfiability problems, in: Proceedings of the 10th National Conference on Artificial Intelligence, AAAI\u201992 (1992) pp. 440\u2013446."},{"issue":"5","key":"421_CR35","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.M. Silva","year":"1999","unstructured":"J.M. Silva and K.A. Sakallah, GRASP: a search algorithm for propositional satisfiability, IEEE Transactions on Computers 48(5) (1999) 506\u2013521.","journal-title":"IEEE Transactions on Computers"},{"key":"421_CR36","doi-asserted-by":"crossref","unstructured":"L. Simon, D. Le Berre and E.A. Hirsch, The SAT2002 Competition, this issue (2004).","DOI":"10.1007\/s10472-005-0424-6"},{"key":"421_CR37","doi-asserted-by":"crossref","unstructured":"L. Simon and P. Chatalic, SATEx: a Web-based framework for SAT experimentation, in: Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001), eds. H. Kautz and B. Selman (Boston University, Boston, MA, 2001).","DOI":"10.1016\/S1571-0653(04)00318-X"},{"key":"421_CR38","doi-asserted-by":"crossref","unstructured":"M.N. Velev and R.E. Bryant, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, in: Proceedings of the 38th Design Automation Conference (DAC\u201901) (2001) pp. 226\u2013231.","DOI":"10.1109\/DAC.2001.935509"},{"key":"421_CR39","first-page":"1","volume":"22","author":"H. Zhang","year":"1993","unstructured":"H. Zhang, A decision procedure for propositional logic, Assoc. Automated Reasoning Newslett. 22 (1993) 1\u20133.","journal-title":"Assoc. Automated Reasoning Newslett."},{"issue":"1\u20132","key":"421_CR40","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1023\/A:1006351428454","volume":"24","author":"H. Zhang","year":"2000","unstructured":"H. Zhang and M. Stickel, Implementing the Davis-Putnam method, Journal of Automated Reasoning 24(1\u20132) (2000) 277\u2013296.","journal-title":"Journal of Automated Reasoning"},{"key":"421_CR41","unstructured":"L. Zheng and P.J. Stuckey, Improving SAT using 2SAT, in: Proceedings of the 25th Australasian Computer Science Conference (ACSC2002), ed. M.J. Oudshoorn, Melbourne, Australia (2002)."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0421-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-005-0421-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0421-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T02:26:49Z","timestamp":1586140009000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-005-0421-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,12,31]]},"references-count":41,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["421"],"URL":"https:\/\/doi.org\/10.1007\/s10472-005-0421-9","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,12,31]]}}}