Fast Algorithms for SAT with Bounded Occurrences of Variables

Fast Algorithms for SAT with Bounded Occurrences of Variables

Junqiang Peng, Mingyu Xiao

Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence
Main Track. Pages 2004-2012. https://doi.org/10.24963/ijcai.2023/223

We present fast algorithms for the general CNF satisfiability problem (SAT) with running-time bound O*({c_d}^n), where c_d is a function of the maximum occurrence d of variables (d can also be the average occurrence when each variable appears at least twice), and n is the number of variables in the input formula. Similar to SAT with bounded clause lengths, SAT with bounded occurrences of variables has also been extensively studied in the literature. Especially, the running-time bounds for small values of d, such as d=3 and d=4, have become bottlenecks for algorithms evaluated by the formula length L and other algorithms. In this paper, we show that SAT can be solved in time O*(1.1238^n) for d=3 and O*(1.2628^n) for d=4, improving the previous results O*(1.1279^n) and O*(1.2721^n) obtained by Wahlström (SAT 2005) nearly 20 years ago. For d>=5, we obtain a running time bound of O*(1.0641^{dn}), implying a bound of O*(1.0641^L) with respect to the formula length L, which is also a slight improvement over the previous bound.
Keywords:
Constraint Satisfaction and Optimization: CSO: Satisfiabilty