On the possibility of faster SAT algorithms

Abstract

We describe reductions from the problem of determining the satisfiability of Boolean CNF formulas (CNF-SAT) to several natural algorithmic problems. We show that attaining any of the following bounds would improve the state of the art in algorithms for SAT: • an O(nk-ε) algorithm for k-DOMINATING SET, for any k ≥ 3, • a (computationally efficient) protocol for 3-party set disjointness with o(m) bits of communication, • an no(d) algorithm for d-SUM, • an O(n2-ε) algorithm for 2-SAT formulas with m = n1+o(1) clauses, where two clauses may have unrestricted length, and • an O((n + m) k-ε) algorithm for HornSat with k unrestricted length clauses. One may interpret our reductions as new attacks on the complexity of SAT, or sharp lower bounds conditional on exponential hardness of SAT. Copyright © by SIAM.