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

DOI:

https://doi.org/10.1609/aaai.v35i5.16487

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.
AAAI-21 Proceedings Cover

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. https://doi.org/10.1609/aaai.v35i5.16487

Issue

Vol. 35 No. 5: AAAI-21 Technical Tracks 5

Section

AAAI Technical Track on Constraint Satisfaction and Optimization