An Improved Upper Bound for SAT

AAAI 2021 pp. 3707-3714

doi:10.1609/AAAI.V35I5.16487 /aaai/2021/chu2021aaai-improved/

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.

PDF AAAI Semantic Scholar

Cite

Text

Chu et al. "An Improved Upper Bound for SAT." AAAI Conference on Artificial Intelligence, 2021. doi:10.1609/AAAI.V35I5.16487

Markdown

[Chu et al. "An Improved Upper Bound for SAT." AAAI Conference on Artificial Intelligence, 2021.](https://mlanthology.org/aaai/2021/chu2021aaai-improved/) doi:10.1609/AAAI.V35I5.16487

BibTeX

@inproceedings{chu2021aaai-improved,
  title     = {{An Improved Upper Bound for SAT}},
  author    = {Chu, Huairui and Xiao, Mingyu and Zhang, Zhe},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2021},
  pages     = {3707-3714},
  doi       = {10.1609/AAAI.V35I5.16487},
  url       = {https://mlanthology.org/aaai/2021/chu2021aaai-improved/}
}