An Improved Upper Bound for SAT

TL;DR

This paper presents a new algorithm for solving CNF SAT more efficiently, reducing the upper bound on the time complexity from previous results by employing amortized analysis and detailed case handling.

Contribution

It introduces an improved upper bound of O*(1.2226^m) for CNF SAT, surpassing earlier bounds by refining analysis techniques.

Findings

Achieved a tighter upper bound of O*(1.2226^m)

Used amortized analysis to optimize algorithm performance

Avoided previous bottlenecks in SAT solving algorithms

Abstract

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