An Improved Upper Bound for SAT

Abstract

We show that the CNF satisfiability problem can be solved $O^{\ast }(1.2226^m)$ time, where $m$ is the number of clauses in the formula, improving the known upper bounds $O^{\ast }(1.234^m)$ given by Yamamoto 15 years ago and $O^{\ast }(1.239^m)$ given by Hirsch 22 years ago. By using an amortized technique and careful case analysis, we successfully avoid the bottlenecks in previous algorithms and get the improvement.