An Improved Upper Bound for SAT

Authors

  • Huairui Chu University of Electronic Science and Technology of China
  • Mingyu Xiao University of Electronic Science and Technology of China
  • Zhe Zhang University of Electronic Science and Technology of China

Keywords:

Satisfiability

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.

Downloads

Published

2021-05-18

How to Cite

Chu, H., Xiao, M., & Zhang, Z. (2021). An Improved Upper Bound for SAT. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5), 3707-3714. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16487

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization