English

An Improved Upper Bound for SAT

Data Structures and Algorithms 2020-07-09 v1 Computational Complexity

Abstract

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

Keywords

Cite

@article{arxiv.2007.03829,
  title  = {An Improved Upper Bound for SAT},
  author = {Huairui Chu and Mingyu Xiao and Zhe Zhang},
  journal= {arXiv preprint arXiv:2007.03829},
  year   = {2020}
}
R2 v1 2026-06-23T16:56:13.046Z