  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.
