{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T02:10:20Z","timestamp":1778033420783,"version":"3.51.4"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2005,5]]},"abstract":"<jats:p>\n            We propose and analyze a simple new randomized algorithm, called ResolveSat, for finding satisfying assignments of Boolean formulas in conjunctive normal form. The algorithm consists of two stages: a preprocessing stage in which resolution is applied to enlarge the set of clauses of the formula, followed by a search stage that uses a simple randomized greedy procedure to look for a satisfying assignment. Currently, this is the fastest known probabilistic algorithm for\n            <jats:italic>k<\/jats:italic>\n            -CNF satisfiability for\n            <jats:italic>k<\/jats:italic>\n            \u2265 4 (with a running time of\n            <jats:italic>O<\/jats:italic>\n            (2\n            <jats:sup>\n              0.5625\n              <jats:italic>n<\/jats:italic>\n            <\/jats:sup>\n            ) for 4-CNF). In addition, it is the fastest known probabilistic algorithm for\n            <jats:italic>k<\/jats:italic>\n            -CNF,\n            <jats:italic>k<\/jats:italic>\n            \u2265 3, that have at most one satisfying assignment (unique\n            <jats:italic>k<\/jats:italic>\n            -SAT) (with a running time\n            <jats:italic>O<\/jats:italic>\n            (2\n            <jats:sup>\n              (2 ln 2 \u2212 1)\n              <jats:italic>n<\/jats:italic>\n              +\n              <jats:italic>o<\/jats:italic>\n              (\n              <jats:italic>n<\/jats:italic>\n              )\n            <\/jats:sup>\n            ) =\n            <jats:italic>O<\/jats:italic>\n            (2\n            <jats:sup>\n              0.386 \u2026\n              <jats:italic>n<\/jats:italic>\n            <\/jats:sup>\n            ) in the case of 3-CNF). The analysis of the algorithm also gives an upper bound on the number of the codewords of a code defined by a\n            <jats:italic>k<\/jats:italic>\n            -CNF. This is applied to prove a lower bounds on depth 3 circuits accepting codes with nonconstant distance. In particular we prove a lower bound \u03a9(2\n            <jats:sup>1.282\u2026\u221a&gt;i&lt;n&gt;\/i&lt;<\/jats:sup>\n            ) for an explicitly given Boolean function of\n            <jats:italic>n<\/jats:italic>\n            variables. This is the first such lower bound that is asymptotically bigger than 2\n            <jats:sup>\n              \u221a&gt;i&lt;n&gt;\/i&lt; +\n              <jats:italic>o<\/jats:italic>\n              (\u221a&gt;i&lt;n&gt;\/i&lt;)\n            <\/jats:sup>\n            .\n          <\/jats:p>","DOI":"10.1145\/1066100.1066101","type":"journal-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:30:55Z","timestamp":1123057855000},"page":"337-364","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":102,"title":["An improved exponential-time algorithm for\n            <i>k<\/i>\n            -SAT"],"prefix":"10.1145","volume":"52","author":[{"given":"Ramamohan","family":"Paturi","sequence":"first","affiliation":[{"name":"University of California San Diego, La Jolla, California"}]},{"given":"Pavel","family":"Pudl\u00e1k","sequence":"additional","affiliation":[{"name":"Mathematical Institute, Academy of Sciences, Prague, Czech Republic"}]},{"given":"Michael E.","family":"Saks","sequence":"additional","affiliation":[{"name":"Rutgers University, Piscataway, New Jersey"}]},{"given":"Francis","family":"Zane","sequence":"additional","affiliation":[{"name":"Bell Labs, Lucent Technologies, Murray Hill, NJ"}]}],"member":"320","published-online":{"date-parts":[[2005,5]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Alon N. Spencer J. and Erd\u00f6s P. 1992. The Probabilistic Method. Wiley New York.  Alon N. Spencer J. and Erd\u00f6s P. 1992. The Probabilistic Method. Wiley New York."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00174-8"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 7th ACM Symposium on Theory of Computing. ACM","author":"Galil Z.","year":"1975","unstructured":"Galil , Z. 1975 . On the validity and complexity of bounded resolution . In Proceedings of the 7th ACM Symposium on Theory of Computing. ACM , New York, 72--82. 10.1145\/800116.803755 Galil, Z. 1975. On the validity and complexity of bounded resolution. In Proceedings of the 7th ACM Symposium on Theory of Computing. ACM, New York, 72--82. 10.1145\/800116.803755"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1017\/S0305004100034241","article-title":"A lower bound for the critical probability in a certain percolation process","volume":"56","author":"Harris T. E.","year":"1960","unstructured":"Harris , T. E. 1960 . A lower bound for the critical probability in a certain percolation process . Proc. Camb. Phil. Soc. 56 , 13 -- 20 . Harris, T. E. 1960. A lower bound for the critical probability in a certain percolation process. Proc. Camb. Phil. Soc. 56, 13--20.","journal-title":"Proc. Camb. Phil. Soc."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 18th ACM Symposium on Theory of Computing. ACM","author":"H\u00e5stad J.","year":"1986","unstructured":"H\u00e5stad , J. 1986 . Almost optimal lower bounds for small depth circuits . In Proceedings of the 18th ACM Symposium on Theory of Computing. ACM , New York, 6--20. 10.1145\/12130.12132 H\u00e5stad, J. 1986. Almost optimal lower bounds for small depth circuits. In Proceedings of the 18th ACM Symposium on Theory of Computing. ACM, New York, 6--20. 10.1145\/12130.12132"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 34th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 124--129","author":"H\u00e5stad J.","unstructured":"H\u00e5stad , J. , Jukna , S. , and Pudl\u00e1k , P . 1993. Top--down lower bounds for depth 3 circuits . In Proceedings of the 34th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 124--129 . H\u00e5stad, J., Jukna, S., and Pudl\u00e1k, P. 1993. Top--down lower bounds for depth 3 circuits. In Proceedings of the 34th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 124--129."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006340920104"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT","author":"Hirsch E.","year":"2002","unstructured":"Hirsch , E. , and Kojevnikov , A . 2002. Unit Walk: A new SAT solver that uses local search guided by unit clause elimination . In Proceedings of 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002 ). 35--42 Hirsch, E., and Kojevnikov, A. 2002. Unit Walk: A new SAT solver that uses local search guided by unit clause elimination. In Proceedings of 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002). 35--42"},{"key":"e_1_2_1_10_1","volume-title":"STACS","volume":"2285","author":"Hofmeister T.","year":"2002","unstructured":"Hofmeister , T. , Sch\u00f6ning , U. , Schuler , R. , and Watanabe , O . 2002. A probabilistic 3-SAT algorithm further improved . In STACS 2002 . Lecture Notes in Computer Science , vol. 2285 . Springer-Verlag, New York, 192--202. Hofmeister, T., Sch\u00f6ning, U., Schuler, R., and Watanabe, O. 2002. A probabilistic 3-SAT algorithm further improved. In STACS 2002. Lecture Notes in Computer Science, vol. 2285. Springer-Verlag, New York, 192--202."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00017-6"},{"key":"e_1_2_1_12_1","unstructured":"Kullmann O. and Luckhardt H. 1998. Algorithms for SAT\/TAUT decision based on various measures. Preprint 81 pages http:\/\/www.cs.utoronto.ca\/kullmann\/.  Kullmann O. and Luckhardt H. 1998. Algorithms for SAT\/TAUT decision based on various measures. Preprint 81 pages http:\/\/www.cs.utoronto.ca\/kullmann\/."},{"key":"e_1_2_1_13_1","unstructured":"MacWilliams F. J. and Sloane N. J. 1977. The Theory of Error-Correcting Codes. North-Holland Amsterdam The Netherland.  MacWilliams F. J. and Sloane N. J. 1977. The Theory of Error-Correcting Codes. North-Holland Amsterdam The Netherland."},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","article-title":"Solving satisfiability in less than 2n steps","volume":"10","author":"Monien B.","year":"1985","unstructured":"Monien , B. , and Speckenmeyer , E. 1985 . Solving satisfiability in less than 2n steps . Discr. Appl. Math. 10 , 287 -- 295 . Monien, B., and Speckenmeyer, E. 1985. Solving satisfiability in less than 2n steps. Discr. Appl. Math. 10, 287--295.","journal-title":"Discr. Appl. Math."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 628--637","author":"Paturi R.","unstructured":"Paturi , R. , Pudl\u00e1k , P. , Saks , M. , and Zane , F . 1998. An improved exponential-time algorithm for k-SAT . In Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 628--637 . Paturi, R., Pudl\u00e1k, P., Saks, M., and Zane, F. 1998. An improved exponential-time algorithm for k-SAT. In Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 628--637."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 566--574","author":"Paturi R.","year":"1999","unstructured":"Paturi , R. , Pudl\u00e1k , P. , and Zane , F . 1997. Satisfiability coding lemma . In Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 566--574 . (See also Chicago J. Theor. Comput. Sci. ( Dec. 1999 ), http:\/\/cjtcs.cs.uchicago.edu\/.) Paturi, R., Pudl\u00e1k, P., and Zane, F. 1997. Satisfiability coding lemma. In Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 566--574. (See also Chicago J. Theor. Comput. Sci. (Dec. 1999), http:\/\/cjtcs.cs.uchicago.edu\/.)"},{"key":"e_1_2_1_17_1","first-page":"598","article-title":"Lower bounds on the size of bounded depth networks over a complete basis with logical addition","volume":"41","author":"Razborov A. A.","year":"1986","unstructured":"Razborov , A. A. 1986 . Lower bounds on the size of bounded depth networks over a complete basis with logical addition . Matematicheskie Zametki 41 , 598 -- 607 (in Russian). (English Translation in Mathematical Notes of the Academy of Sciences of the USSR 41, 333--338.) Razborov, A. A. 1986. Lower bounds on the size of bounded depth networks over a complete basis with logical addition. Matematicheskie Zametki 41, 598--607 (in Russian). (English Translation in Mathematical Notes of the Academy of Sciences of the USSR 41, 333--338.)","journal-title":"Matematicheskie Zametki"},{"key":"e_1_2_1_18_1","series-title":"Lecture Notes in Computer Science","volume-title":"Selected papers from CSL '92","author":"Schiermeyer I.","unstructured":"Schiermeyer , I. 1993. Solving 3-satisfiability in less than 1.579n steps . In Selected papers from CSL '92 . Lecture Notes in Computer Science , vol. 702 . Springer-Verlag , New York , 379--394. Schiermeyer, I. 1993. Solving 3-satisfiability in less than 1.579n steps. In Selected papers from CSL '92. Lecture Notes in Computer Science, vol. 702. Springer-Verlag, New York, 379--394."},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 40th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 410--414","author":"Sch\u00f6ning U.","year":"1999","unstructured":"Sch\u00f6ning , U. 1999 . A probabilistic algorithm for k-SAT and constraint satisfaction problems . In Proceedings of the 40th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 410--414 . Sch\u00f6ning, U. 1999. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In Proceedings of the 40th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 410--414."},{"key":"e_1_2_1_20_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 6th Symposium on Mathematical Foundations of Computer Science","author":"Valiant L. G.","unstructured":"Valiant , L. G. 1977. Graph-theoretic arguments in low-level complexity . In Proceedings of the 6th Symposium on Mathematical Foundations of Computer Science , Lecture Notes in Computer Science , vol. 53 , Springer-Verlag , New York , 162--176. Valiant, L. G. 1977. Graph-theoretic arguments in low-level complexity. In Proceedings of the 6th Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 53, Springer-Verlag, New York, 162--176."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00144-1"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1066100.1066101","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1066100.1066101","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:17Z","timestamp":1750262897000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1066100.1066101"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["10.1145\/1066100.1066101"],"URL":"https:\/\/doi.org\/10.1145\/1066100.1066101","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,5]]},"assertion":[{"value":"2005-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}