Further Improvements for SAT in Terms of Formula Length

TL;DR

This paper presents an improved algorithm for solving CNF satisfiability problems with a faster exponential time complexity of O^*(1.0638^L), achieved through advanced branching rules and amortized analysis techniques.

Contribution

It introduces new branching strategies and analytical frameworks that improve the time complexity for CNF SAT solving based on formula length.

Findings

Achieved a time complexity of O^*(1.0638^L) for CNF SAT.

Developed new branching rules for degree-4 and degree-5 variables.

Provided general analysis frameworks and lower bounds for measure decrease.

Abstract

In this paper, we prove that the general CNF satisfiability problem can be solved in $O^*(1.0638^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 previous result of $O^*(1.0652^L)$ obtained in 2009. Our algorithm was analyzed by using the measure-and-conquer method. Our improvements are mainly attributed to the following two points: we carefully design branching rules to deal with degree-5 and degree-4 variables to avoid previous bottlenecks; we show that some worst cases will not always happen, and then we can use an amortized technique to get further improvements. In our analyses, we provide some general frameworks for analysis and several lower bounds on the decreasing of the measure to simplify the arguments. These techniques may be used to analyze more algorithms based on the measure-and-conquer method.