{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:01Z","timestamp":1749125401492,"version":"3.41.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2000,2]]},"DOI":"10.1023\/a:1006318521185","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:36:27Z","timestamp":1040520987000},"page":"127-143","source":"Crossref","is-referenced-by-count":21,"title":["SAT Local Search Algorithms: Worst-Case Study"],"prefix":"10.1007","volume":"24","author":[{"given":"Edward A.","family":"Hirsch","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"255306_CR1","doi-asserted-by":"crossref","unstructured":"Cook, S. and Reckhow, R.: On the lengths of proofs in the propositional calculus (preliminary version), in Conference Record of Sixth Annual ACM Symposium on Theory of Computing, 1974, pp. 135\u2013148.","DOI":"10.1145\/800119.803893"},{"key":"255306_CR2","doi-asserted-by":"crossref","first-page":"1293","DOI":"10.1007\/BF01084392","volume":"22","author":"E. Dantsin","year":"1983","unstructured":"Dantsin, E.: Two systems for proving tautologies, based on the split method, J. Soviet Math.\n22 (1983), 1293\u20131305.","journal-title":"J. Soviet Math."},{"key":"255306_CR3","unstructured":"Dubois, O., Boufkhad, Y. and Mandler, J.: Typical random 3-SAT formulae and the satisfiability threshold. To appear in Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms, 2000."},{"key":"255306_CR4","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1006\/jagm.1996.0016","volume":"20","author":"A. Frieze","year":"1996","unstructured":"Frieze, A. and Suen, S.: Analysis of two simple heuristics on a random instance of k-SAT, J. Algorithms\n20 (1996), 312\u2013355.","journal-title":"J. Algorithms"},{"key":"255306_CR5","unstructured":"Gent, I. and Walsh, T.: The enigma of hill-climbing procedures for SAT, Research Paper 605, Department of Artificial Intelligence, University of Edinburgh, 1992."},{"key":"255306_CR6","first-page":"28","volume-title":"Proceedings of the 11th National Conference on Artificial Intelligence","author":"I. Gent","year":"1993","unstructured":"Gent, I. and Walsh, T.: Towards an understanding hill-climbing procedures for SAT, in Proceedings of the 11th National Conference on Artificial Intelligence, Washington, DC, AAAI Press, 1993, pp. 28\u201333."},{"key":"255306_CR7","volume-title":"Hybrid Problems, Hybrid Solutions (AISB-95)","author":"I. Gent","year":"1995","unstructured":"Gent, I. and Walsh, T.: Unsatisfied variables in local search, in J. Hallam (ed.), Hybrid Problems, Hybrid Solutions (AISB-95), IOS Press, Amsterdam, 1995."},{"key":"255306_CR8","doi-asserted-by":"crossref","unstructured":"Gu, J. and Gu, Q.-P.: Average time complexity of the SAT1.2 algorithm, in Proceedings of the 5th Annual International Symposium on Algorithms and Computation, 1994, pp. 147\u2013155.","DOI":"10.1007\/3-540-58325-4_176"},{"key":"255306_CR9","unstructured":"Hirsch, E. A.: Two new upper bounds for SAT, in Proceedings of the 9th Annual ACM-SIAM Symposium on Discrete Algorithms, 1998, pp. 521\u2013530. An improved journal version is to appear in J. Automated Resoning special issue \u201cSAT-2000\u201d."},{"key":"255306_CR10","doi-asserted-by":"crossref","unstructured":"Hirsch, E. A.: Local search agorithms for SAT: Worst-case analysis, in Proceedings of the 6th Scandinavian Workshop on Algorithm Theory, Lecture Notes in Comput. Sci. 1432, 1998, pp. 246\u2013254.","DOI":"10.1007\/BFb0054372"},{"key":"255306_CR11","unstructured":"Hoos, H. H. and St\u00fctzle, T.: Local search algorithms for SAT: An empirical evaluation. To appear in J. Automated Reasoning special issue \u201cSAT-2000\u201d."},{"issue":"3","key":"255306_CR12","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1002\/(SICI)1098-2418(199805)12:3<253::AID-RSA3>3.0.CO;2-U","volume":"12","author":"L. M. Kirousis","year":"1998","unstructured":"Kirousis, L. M., Kranakis, E., Krizanc, D. and Stamatiou, Y. C.: Approximating the unsatisfiability threshold of random formulas, Random Structures Algorithms\n12(3) (1998), 253\u2013269.","journal-title":"Random Structures Algorithms"},{"issue":"1","key":"255306_CR13","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0020-0190(92)90029-U","volume":"43","author":"E. Koutsoupias","year":"1992","unstructured":"Koutsoupias, E. and Papadimitriou, C. H.: On the greedy algorithm for satisfiability, Inform. Process. Lett.\n43(1) (1992), 53\u201355.","journal-title":"Inform. Process. Lett."},{"issue":"1\u20132","key":"255306_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(98)00017-6","volume":"223","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: New methods for 3-SAT decision and worst-case analysis, Theoret. Comput. Sci.\n223(1\u20132) (1999), 1\u201372.","journal-title":"Theoret. Comput. Sci."},{"key":"255306_CR15","unstructured":"McAllester, D., Selman, B. and Kautz, H.: Evidence for invariants in local search, in Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference, Providence, RI, AAAI Press, 1997, pp. 321\u2013326."},{"key":"255306_CR16","unstructured":"Mitchell, D. G., Selman, B. and Levesque, H.: Hard and easy distributions of SAT problems, in Proceedings of the Tenth National Conference on Artificial Intelligence, San Jose, California, AAAI Press\/MIT Press, 1992, pp. 459\u2013465."},{"key":"255306_CR17","unstructured":"Monien, B. and Speckenmeyer, E.: 3-satisfiability is testable in O.1:62r \/ steps, Bericht Nr. 3\/1979, Reihe Theoretische Informatik, Universit\u00e4t-Gesamthochschule-Paderborn."},{"key":"255306_CR18","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","volume":"10","author":"B. Monien","year":"1985","unstructured":"Monien, B. and Speckenmeyer, E.: Solving satisfiability in less than 2n steps, Discrete Appl. Math.\n10 (1985), 287\u2013295.","journal-title":"Discrete Appl. Math."},{"key":"255306_CR19","unstructured":"Papadimitriou, Ch. H.: Computational Complexity, Addison-Wesley, 1994."},{"key":"255306_CR20","doi-asserted-by":"crossref","unstructured":"Paturi, R., Pudlak, P., Saks, M. E. and Zane, F.: An improved exponential-time algorithm for k-SAT, in Proceedings of the 39th Annual Symposium on Foundations of Computer Science, 1998, pp. 628\u2013637.","DOI":"10.1109\/SFCS.1998.743513"},{"key":"255306_CR21","unstructured":"Schiermeyer, I.: Pure literal look ahead: An O(1:497n) 3-satisfiability algorithm, in J. Franco, G. Gallo, H. Kleine B\u00fcning, E. Speckenmeyer and C. Spera (eds.), Workshop on the Satisfiability Problem, Technical Report, Siena, 29 April-3 May, 1996. University K\u00f6ln, Report No. 96\u2013230."},{"key":"255306_CR22","unstructured":"Sch\u00f6ning, U.: A probabilistic algorithm for k-SAT and constraint satisfaction problems. To appear in Proceedings of the 40th Annual Symposium on Foundations of Computer Science, 1999."},{"key":"255306_CR23","volume-title":"Proceedings of the 11th National Conference on Artificial Intelligence","author":"B. Selman","year":"1993","unstructured":"Selman, B. and Kautz, H.: An empirical study of greedy local search for satisfiability testing, in Proceedings of the 11th National Conference on Artificial Intelligence, Washington, DC, AAAI Press, 1993."},{"key":"255306_CR24","unstructured":"Selman, B. and Kautz, H.: Pushing the envelope: Planning, propositional logic, and stochastic search, in Proceedings of the 14th Conference on Artificial Intelligence, 1996."},{"key":"255306_CR25","first-page":"337","volume-title":"Proceedings of the 12th National Conference on Artificial Intelligence","author":"B. Selman","year":"1994","unstructured":"Selman, B., Kautz, H. and Cohen, B.: Noise strategies for improving local search, in Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, Washington, AAAI Press, 1994, pp. 337\u2013343."},{"key":"255306_CR26","unstructured":"Selman, B., Kautz, H. and Cohen, B.: Local search strategies for satisfiability testing, in Second DIMACS Challenge on Cliques, Coloring and Satisfiability, 1993. A version of this paper is to appear in DIMACS Series in Discrete Mathematics."},{"key":"255306_CR27","first-page":"440","volume-title":"Proceedings of the 10th National Conference on Artificial Intelligence","author":"B. Selman","year":"1992","unstructured":"Selman, B., Levesque, H. and Mitchell, D.: A new method for solving hard satisfiability problems, in W. Swartout (ed.), Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, California, MIT Press, 1992, pp. 440\u2013446."},{"issue":"4","key":"255306_CR28","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2307\/421131","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs, Bulletin of Symbolic Logic\n1(4) (1995), 425\u2013467.","journal-title":"Bulletin of Symbolic Logic"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006318521185.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006318521185\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006318521185.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:28:11Z","timestamp":1749122891000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006318521185"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,2]]},"references-count":28,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,2]]}},"alternative-id":["255306"],"URL":"https:\/\/doi.org\/10.1023\/a:1006318521185","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2000,2]]}}}