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.

翻译：我们证明了CNF可满足性问题（SAT）可以在$O^*(1.1199^{(d-2)n})$时间内求解，其中$d$为任一变量的最大出现次数，或者当不存在仅出现一次的变量时，为所有变量的平均出现次数。该结果改进了Wahlstr$\ddot{\text{o}}$m（SAT 2005）提出的$O^*(1.1279^{(d-2)n})$上界以及Peng和Xiao（IJCAI 2023）提出的$O^*(1.1238^{(d-2)n})$上界。对于$d\leq 4$的情况，我们的算法优于先前结果。我们的主要技术贡献是提出了一种针对3-occur-SAT（即所有变量最多出现3次的SAT受限实例）的算法，其时间复杂度为$O^*(1.1199^n)$。通过更深入的案例分析以及一种能在较宽泛条件下消解多个变量的归约规则，我们成功规避了先前算法中的瓶颈。