An Improved Algorithm for Sparse Instances of SAT

TL;DR

This paper presents an improved algorithm for solving SAT instances with bounded variable occurrences, achieving faster runtimes than previous methods, especially for instances where variables occur at most three times.

Contribution

The authors develop a new algorithm that improves the upper bound for solving SAT with bounded variable occurrences, notably for cases with up to three occurrences per variable.

Findings

Achieves a runtime of $O^*(1.1199^n)$ for 3-occur-SAT.

Improves the upper bound for SAT with bounded variable occurrences over previous work.

Effective case analysis and reduction rules enable circumventing previous algorithmic bottlenecks.

Abstract

We show that the CNF satisfiability problem (SAT) can be solved in time $O^*(1.1199^{(d-2)n})$, where $d$ is either the maximum number of occurrences of any variable or the average number of occurrences of all variables if no variable occurs only once. This improves upon the known upper bound of $O^*(1.1279^{(d-2)n})$ by Wahlstr$\ddot{\text{o}}$m (SAT 2005) and $O^*(1.1238^{(d-2)n})$ by Peng and Xiao (IJCAI 2023). For $d\leq 4$, our algorithm is better than previous results. Our main technical result is an algorithm that runs in $O^*(1.1199^n)$ for 3-occur-SAT, a restricted instance of SAT where all variables have at most 3 occurrences. Through deeper case analysis and a reduction rule that allows us to resolve many variables under a relatively broad criteria, we are able to circumvent the bottlenecks in previous algorithms.