An Improved Algorithm for Sparse Instances of SAT

TL;DR

Through deeper case analysis and a reduction rule that allows us to resolve many variables under a relatively broad criteria, the CNF satisfiability problem (SAT) can be solved in time and is able to circumvent the bottlenecks in previous algorithms.

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.

Figures (1)

• Figure 1: Example of Step 6d of the algorithm and lemma \ref{['key reduction']}. In stage 1, we have $F_{contain \{x,y,a,b,c,d\}}$ and the maximal subclauses (without $\{x,y,a,b,c,d\}$) $C_1, C_2, C_3$. In stage 2, we have the clauses after resolving variables in $\{x,y,a,b,c,d\}$. In stage 3, we remove the redundant clause after standardization. In stage 4, we introduce 3 new variables $v_1,v_2,v_3$ to reduce the occurrences of our maximal subclauses back to 1.

Theorems & Definitions (52)

• Definition 1
• Definition 2: Safe resolution
• Lemma 4.1
• proof
• Lemma 4.2
• proof
• Lemma 4.3
• proof
• Lemma 4.4
• proof