This paper establishes a randomized algorithm that finds a satisfying assignment for a satisfiable formula F in 3-CNF in O (1 3279 3 n ) expected running time. The algorithms is based on the analysis of so-called strings, which are sequences of 3-clauses where non-succeeding clauses do not share a variable and succeeding clauses share one or two variables. One the one hand, if there are not many independent strings, we can solve F with a decent success probability, but on the other hand, if there are many strings, we use them to improve the running time of Sch?ning's 3-SAT algorithm. Within a string, propagation of unit clauses is used to find successors.
展开▼
