References & Citations
Computer Science > Data Structures and Algorithms
Title: A Fast Algorithm for SAT in Terms of Formula Length
(Submitted on 13 May 2021 (this version), latest version 17 Aug 2022 (v2))
Abstract: In this paper, we prove that the general CNF satisfiability problem can be solved in $O^*(1.0646^L)$ time, where $L$ is the length of the input CNF-formula (i.e., the total number of literals in the formula), which improves the current bound $O^*(1.0652^L)$ given by Chen and Liu 12 years ago. Our algorithm is a standard branch-and-search algorithm analyzed by using the measure-and-conquer method. We avoid the bottleneck in Chen and Liu's algorithm by simplifying the branching operation for 4-degree variables and carefully analyzing the branching operation for 5-degree variables. To simplify case-analyses, we also introduce a general framework for analysis, which may be able to be used in other problems.
Submission history
From: Mingyu Xiao [view email][v1] Thu, 13 May 2021 08:15:56 GMT (44kb)
[v2] Wed, 17 Aug 2022 15:02:02 GMT (320kb)
Link back to: arXiv, form interface, contact.