Improved Upper Bounds for 3-SAT
Kazuo Iwama, Suguru Tamaki · 2003
The CNF Satisfiability 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 exists a lot of algorithms which run significantly 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 first local search algorithm which gives a guaranteed performance for general instances and [DGH+02], [HSSW02], [BS03] and [Rol03] follow up this Schöning’s approach. 3-SAT 4-SAT 5-SAT 6-SAT type ref. 1.782 1.835 1.867 1.888 det. [PPZ97]