An improved exponential-time algorithm for $\textit{k}-SAT$An improved exponential-time algorithm for $\textit{k}-SAT$

Access Restriction
Subscribed

 Author Paturi, Ramamohan ♦ Pudlk, Pavel ♦ Saks, Michael E. ♦ Zane, Francis Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2005 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Subject Keyword CNF satisfiability ♦ Randomized algorithms Abstract 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 $\textit{k}-CNF$ satisfiability for $\textit{k}$ ≥ 4 (with a running time of $O(2^{0.5625n})$ for 4-CNF). In addition, it is the fastest known probabilistic algorithm for $\textit{k}-CNF,$ $\textit{k}$ ≥ 3, that have at most one satisfying assignment (unique $\textit{k}-SAT)$ (with a running time $\textit{O}(2(2$ ln 2 ™ $1)\textit{n}$ + $\textit{o}(\textit{n}))$ = $\textit{O}(20.386$ … $\textit{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 $\textit{k}-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 $Ω(2^{1.282…√>i/i<})$ for an explicitly given Boolean function of $\textit{n}$ variables. This is the first such lower bound that is asymptotically bigger than 2√>i/i< + $\textit{o}(√>i/i<).$ ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2005-05-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 52 Issue Number 3 Page Count 28 Starting Page 337 Ending Page 364

Open content in new tab

Source: ACM Digital Library