Improved upper bounds for 3-SAT

The CNF Satisability problem is to determine, given a CNF formula F, whether or not there exists a satisfying assignment for F. If each clause of F contains at most k literals, then F is called a k-CNF formula and the problem is called k-SAT. For small k's, especially for k = 3, there have been a lot of algorithms which run signicantly faster than the trivial 2n bound. The following list summarizes those algorithms where a constant c means that the algorithm runs in time O(cn). Roughly speaking most algorithms are based on Davis-Putnam. [Sch99] is the rst local search algorithm which gives a guaranteed performance for general instances and [DGH+02], [HSSW02] and [BS03] follow up this Schoning's approach. 3-SAT 4-SAT 5-SAT 6-SAT type ref. 1.782 1.835 1.867 1.888 det. [PPZ97