An Improved Upper Bound for SAT

Abstract

We show that the CNF satisfiability problem can be solved O*(1.2226m) time, where m is the number of clauses in the formula, improving the known upper bounds O*(1.234m) given by Yamamoto 15 years ago and O*(1.239m) 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.