2024/11/11 by Sanjay Jain, Jain, Sanjay, Tzeh Yuan Neoh +3
Computer Science · #Advanced Database Systems and Queries #Constraint Satisfaction and Optimization #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences
paper · pdf · doi:10.48550/arxiv.2411.07389
openalex publication_date 2024/11/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 Wahlstrom (SAT 2005) and O^*(1.1238(d-2)n) by Peng and Xiao (IJCAI 2023). For d≤ 4, our algorithm is better than previous results. Our main technical result is an algorithm that runs in O^*(1.1199n) 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.