\section{Introduction}
Propositional Satisfiability is the problem of determining, for a formula of the propositional calculus, if there is an assignment of truth values to its variables for which that formula evaluates to true. By SAT, we mean the problem of propositional satisfiability for formulas in conjunctive normal form (CNF)~\cite{DBLP:conf/dimacs/CookM96}. The SAT problem is the first problem proved to be NP-complete~\cite{DBLP:conf/stoc/Cook71} and it plays an important role in computational complexity and artificial intelligence~\cite{DBLP:series/faia/2009-185}. There are numerous investigations on this problem in different fields, such as approximation algorithms, randomized algorithms, heuristic algorithms, and exact and parameterized algorithms.
In this paper, we study parameterized algorithms for SAT parameterized by the input length.


To measure the running time bound for the SAT problem, there are three frequently used parameters: the number of variables $n$, the number of clauses $m$, and the input length $L$. The input length $L$ is defined as the sum of the number of literals in each clause.
The number of variables $n$ should be the most basic parameter. The simple brute force algorithm to try all $2^n$ possible assignments of the $n$ variables will get the running time bound of $O^*(2^n)$.\footnote{The $O^*$ notation supervises all polynomial factors, i.e., $f(n)=O^*(g(n))$ means $f(n)=O(g(n)n^{O(1)})$.}
After decades of hard work, no one can break this trivial bound.
The Strong Exponential Time Hypothesis conjectures that the SAT problem cannot be solved in time $O^*(c^n)$ for some constant $c<2$~\cite{DBLP:journals/jcss/ImpagliazzoP01}.
For a restricted version, the $k$-SAT problem (the length of each clause in the formula is bounded by a constant $k$), better results have been developed. For example, 3-SAT can be solved in $O^*(1.3279^n)$ time~\cite{DBLP:conf/icalp/Liu18}, 4-SAT can be solved in $O^*(1.4986^n)$ time~\cite{DBLP:conf/icalp/Liu18}, and $k$-SAT can be solved in $O^*(c(k)^n)$ time for some value $c(k)$ depending on $k$~\cite{DBLP:conf/icalp/Liu18}.
When it comes to the parameter $m$, Monien \textit{et al.} first gave an algorithm with time complexity $O^*(1.260^m)$ in 1981~\cite{monien1981upper}. Later, the bound was improved to $O^*(1.239^m)$ by Hirsch in 1998~\cite{DBLP:conf/soda/Hirsch98}, and then
improved to $O^*(1.234^m)$ by Yamamoto in 2005~\cite{DBLP:conf/isaac/Yamamoto05}. Now the best result is $O^*(1.2226^m)$ obtained by Chu, Xiao, and Zhang~\cite{DBLP:conf/aaai/SATM2020}.


The input length $L$ is another important and frequently studied parameter. It is probably the most precise parameter to describe the input CNF-Formula.  From the first algorithm with running time bound $O^*(1.0927^L)$ by Van Gelder in 1988~\cite{DBLP:journals/iandc/Gelder88}, the result was improved several times. In 1997, the bound was improved to $O^*(1.0801)$ by Kullmann and Luckhardt~\cite{kullmann1997deciding}. In 1998, the bound was improved to $O^*(1.0758^L)$ by Hirsch~\cite{DBLP:conf/soda/Hirsch98}, and improved again by Hirsch to $O^*(1.074^L)$ in 2000~\cite{DBLP:journals/jar/Hirsch00a}. Then Wahlstr{\"{o}}m gave an $O^*(1.0663^L)$-time algorithm in 2005~\cite{DBLP:conf/esa/Wahlstrom05}. In 2009, Chen and Liu~\cite{DBLP:conf/wads/ChenL09} used the measure-and-conquer method to analyze the running time bound and further improved the result to $O^*(1.0652^L)$. We list the major progress and our result in Table \ref{tb-result-L}.

\begin{table}[t]\label{tb-result-L}
\begin{center}
\caption{Previous and our upper bound for SAT}
\begin{tabular}{l|c}
    \hline
    Running time bounds & References \\
    \hline
    $O^*(1.0927^L)$ & Van Gelder~1988~\cite{DBLP:journals/iandc/Gelder88} \\
    $O^*(1.0801^L)$ & Kullmann and Luckhardt~1997~\cite{kullmann1997deciding} \\
    $O^*(1.0758^L)$ & Hirsch~1998~\cite{DBLP:conf/soda/Hirsch98}\\
    $O^*(1.074^L)$ & Hirsch~2000~\cite{DBLP:journals/jar/Hirsch00a} \\
    $O^*(1.0663^L)$ & Wahlstr{\"{o}}m~2005~\cite{DBLP:conf/esa/Wahlstrom05} \\
    $O^*(1.0652^L)$ & Jianer Chen and Yang Liu~2009~\cite{DBLP:conf/wads/ChenL09}\\
    $O^*(1.0646^L)$ & \textbf{This paper~2021} \\
    \hline
\end{tabular}
\end{center}
\end{table}

Our algorithm, as well as most algorithms for the SAT problem, is based on the branch-and-search process.
The idea of branch-and-search is simple and practical: for a given CNF-formula $\mathcal{F}$, we iteratively branch on a variable or literal $x$ into two branches by assigning value 1 or 0 to it. Let $\mathcal{F}_{x=1}$ and $\mathcal{F}_{\overline{x}=1}$ be the resulted CNF-formula by assigning value 1 and 0 to $x$, respectively. It holds that $\mathcal{F}$ is satisfiable if and only if at least one of $\mathcal{F}_{x=1}$ and $\mathcal{F}_{\overline{x}=1}$ is satisfiable. To get a running time bound, we need to analyze how much the parameter $L$ can decrease in each branch. To break some bottlenecks in direct analysis, some references~\cite{DBLP:conf/esa/Wahlstrom05,DBLP:conf/wads/ChenL09} analyzed
the algorithm based on some other measures and gave the relation between the new measure and $L$. The current best result~\cite{DBLP:conf/wads/ChenL09} was obtained by using the measure-and-conquer method, which is also to use a new measure. This is the first time to bring the measure-and-conquer method to this research line. In this paper, we further improve the running time bound by still using the measure-and-conquer method.
Similar to many measure-and-conquer algorithms, our algorithm and the algorithm in~\cite{DBLP:conf/wads/ChenL09} deal with variables from high degree to low degree.
The algorithm in~\cite{DBLP:conf/wads/ChenL09} carefully analyzed branching operations for variables of degree 4. Our algorithm will simplify the branching operation for 4-degree variables and carefully analyze the branching operation for 5-degree variables. Finally, we can improve the bound to $O^*(1.0646^L)$.


\section{Preliminaries}
Let $V = \{x_1, x_2, ..., x_n\}$ denote a set of $n$ boolean \emph{variables}.
Each variable $x_i$ ($i \in \{1, 2, ..., n\}$) has two corresponding \textit{literals}: positive literal $x_i$ and negative literal $\overline{x_i}$ (we use $\overline{x}$ to denote the negation of a literal $x$, and $\overline{\overline{x}}=x$).
A \textit{clause} on $V$ consists of some literals on $V$.
Note that we allow a clause to be empty.
A clause $\{z_1,z_2,\dots, z_q\}$ is also simply written as $z_1z_2\dots z_q$. Thus, we use $zC$ to denote the clause containing literal $z$ and all literals in clause $C$. We also use $C_1C_2$ to denote the clause containing all literals in clauses $C_1$ and $C_2$.
We use $\overline{C}$ to denote a clause that contains the negation of every literal in clause $C$. That is, if $C=z_1z_2...z_q$, then $\overline{C} = \overline{z_1}\overline{z_2}...\overline{z_q}$.
A \emph{CNF-formula} on $V$ is the conjunction of a set of clauses $\mathcal{F} = \{C_1, C_2,  ..., C_m\}$. When we say a variable $x$ is contained in a clause (or a formula), it means that the clause (at least one clause of the formula) contains a literal $x$ or its negative  $\overline{x}$.


An assignment for $V$ is a map $A: V\rightarrow \{0, 1\}$. A clause $C_j$ is \textit{satisfied} by an assignment if and only if there exists at least one literal in $C_j$ such that the assignment makes its value 1. A CNF-formula is \emph{satisfied} by an assignment $A$ if and only if each clause in it is satisfied by $A$. We say a CNF-formula is \textit{satisfiable} if it can be satisfied by at least one assignment.
We may assign value 0 or 1 to a literal, which is indeed to assign a value to its variable to make the corresponding literal 0 or 1.



A literal $z$ is called an \textit{$(i, j)$-literal} (resp., an \textit{$(i^+, j)$-literal} or \textit{$(i^-, j)$-literal}) in a formula $\mathcal{F}$ if $z$ appears $i$ (resp. at least $i$ or at most $i$) times and $\overline{z}$ appears $j$ times in the formula $\mathcal{F}$. Similarly, we can define $(i, j^+)$-literal, $(i, j^-)$-literal, $(i^+, j^+)$-literal, $(i^-, j^-)$-literal, and so on.
Note that literal $z$ is an $(i, j)$-literal if and only if literal $\overline{z}$ is a $(j, i)$-literal.
A variable $x$ is an \textit{$(i, j)$-variable} if the positive literal $x$ is an $(i, j)$-literal.
For a variable or a literal $x$ in formula $\mathcal{F}$, the \textit{degree} of it, denoted by $deg(x)$, is the number of $x$ appearing in $\mathcal{F}$ plus the number of $\overline{x}$ appearing in $\mathcal{F}$, i.e., $deg(x)=i+j$ for an $(i, j)$-variable or $(i, j)$-literal $x$.
A \textit{$d$-variable} (resp., \emph{$d^+$-variable} or \emph{$d^-$-variable}) is a variable with the degree exactly $d$ (resp., at least $d$ or at most $d$). The degree of a formula $\mathcal{F}$ is the maximum degree of all variables in $\mathcal{F}$. For a clause or a formula $C$, the set of variables whose literal appears in $C$ is denoted by $var(C)$.

The $\textit{length}$ of a clause $C$, denoted by $|C|$, is the number of literals in $C$. A clause is a \textit{$k$-clause} or \textit{$k^+$-clause} if the length of it is $k$ or at least $k$. We use $L(\mathcal{F})$ to indicate the length of a formula $\mathcal{F}$. It is the sum of the lengths of all clauses in $\mathcal{F}$, which is also the sum of the degrees of all variables in $\mathcal{F}$. A formula $\mathcal{F}$ is called \textit{$k$-CNF formula} if each clause in $\mathcal{F}$ has a length of at most $k$.

In a formula $\mathcal{F}$, a literal $x$ is called a \emph{neighbor} of a literal $z$ if there is a clause containing both $z$ and $x$. The set of neighbors of a literal $z$ in a formula $\mathcal{F}$ is denoted by \textit{$N(z, \mathcal{F})$}. We also use $N^{(k)}(x, \mathcal{F})$ (resp., $N^{(k+)}(z, \mathcal{F})$) to denote the neighbors of $z$ in $k$-clauses (resp., $k^+$-clauses) in $\mathcal{F}$, \textit{i.e.}, for any $z'\in N^{(k)}(z, \mathcal{F})$ (resp., $z'\in N^{(k+)}(z, \mathcal{F})$), there exists a $k$-clause (resp., $k^+$-clause) containing both $z$ and $z'$.



\section{Branch-\&-Search and Measure-\&-Conquer}
Our algorithm is a standard branch-and-search algorithm, which first applies some reduction rules to reduce the instance as much as possible and then searches for a solution by branching. The branching operations may exponentially increase the running time.
We will use a measure to evaluate the size of the search tree generated in the algorithm.
For the SAT problem, the number of variables or clauses of the formula is a commonly used measure.
More fundamentals of branching heuristics about the SAT problem can be found in~\cite{DBLP:series/faia/2009-185}.

We use $T(\mu)$ to denote the maximum size or number of leaves of the search tree generated by the algorithm for any instance with the measure being at most $\mu$. For a branching operation that branches on the current instance into $l$ branches with
the measure decreasing by at least $a_i$ in the $i$-th branch, we get a
 a recurrence relation
\[T(\mu)\leq T(\mu-a_1)+T(\mu-a_2)+\dots + T(\mu-a_l).\]
The recurrence relation can also be simply represented by a \emph{branching vector} $[a_1,a_2,\dots,a_l]$.
The largest root of the function $f(x) = 1-\sum_{i=1}^lx^{-a_i}$ is called the \emph{branching factor} of the recurrence.
If the maximum branching factor for all branching operations in the algorithm is at most $\gamma$,
then $T(\mu)=O(\gamma^\mu)$. If on each node of the search tree, the algorithm runs in polynomial time, then the total running time of the algorithm is $O^*(\gamma^\mu)$.
For two branching vectors $\mathbf{a}=[a_1,a_2,\dots,a_l]$ and $\mathbf{b}=[b_1,b_2,\dots,b_l]$, if $a_i\geq b_i$ holds for all $i=1,2\dots,l$, then the branching factor of $\mathbf{a}$ is not greater than that of $\mathbf{b}$.
For this case, we say $\mathbf{b}$ \emph{dominates} $\mathbf{a}$.
This property will be used in many places to simplify some arguments in the paper.
More details about analyzing recurrences can be found in the monograph~\cite{DBLP:series/txtcs/FominK10}.

The measure-and-conquer method \cite{DBLP:journals/jacm/FominGK09} is a powerful tool to analyze branch-and-search algorithms.
The main idea of the method is to adopt a new measure in the analysis of the algorithm. For example, instead of using the number of variables as the measure, it may set weights to different variables and use the sum of all variable weights as the measure. This method may be able to catch more structural properties and then get further improvements. Nowadays, the fastest exact algorithms for many NP-hard problems were designed by using this method. In this paper, we will also use the measure-and-conquer method.

We introduce a weight to each variable in the formula according to the degree of the variable, $w\colon\mathbb{Z}^+ \rightarrow \mathbb{R}^+$, where $\mathbb{Z}^+$ and $\mathbb{R}^+$ denote the sets of nonnegative integers and nonnegative reals, respectively. Let $w_i$ denote the weight of a variable with degree $i$.
A variable with lower degree will not receive a higher weight. \textit{i.e.}, $w_i\geq w_{i-1}$.
In our algorithm, the measure of a formula $\mathcal{F}$ is defined as
\begin{equation}\label{measure}
    \mu(\mathcal{F}) = \sum_{x} w_{deg(x)}.
\end{equation}
In other words, $\mu(\mathcal{F})$ is the sum of the weight of all variables in $\mathcal{F}$.
Let $n_i$ denote the number of $i$-variables in $\mathcal{F}$. Then we also have that
 $\mu(\mathcal{F})=\sum_{i} w_in_i$.

One important step is to set the value of weight $w_i$. Different values of $w_i$ will generate different branching vectors and factors. We need to find a good setting of $w_i$ so that the worst branching factor is as small as possible.
We will get the value of $w_i$ by solving a quasiconvex program after listing all our branching vectors. However, we pre-specify some requirements of the weights to simplify arguments. Some similar assumptions were used in previous measure-and-conquer algorithms. We set the weight such that
\begin{equation}\label{weight1}
\begin{aligned}
     &w_1=w_2=0,\\
     &0<w_3< 2, w_4= 2w_3, ~\text{and}\\
     &w_i = i  ~\text{for }~ i\geq 5.
\end{aligned}
\end{equation}
We use $\delta_i$ to denote the difference between $w_i$ and $w_{i-1}$ for $i > 0$, \textit{i.e.}, $\delta_i=w_i-w_{i-1}$.
By (\ref{weight1}), we have
\begin{equation}\label{eq-w3-d3-d4}
    w_3=\delta_3=\delta_4.
\end{equation}
We also assume that
\begin{equation}\label{weight2}
\begin{aligned}
    & \delta_i \leq \delta_{i-1} ~\text{for}~i\geq 3,~\text{and}\\
    & w_3\geq \delta_5. &
\end{aligned}
\end{equation}

Under these assumptions, it holds that $w_i\leq i$ for each $i$. Thus, we have
\begin{equation}\label{measure-leq-L}
    \mu(\mathcal{F}) \leq L(\mathcal{F}).
\end{equation}
This tells us that if we can get a running time bound of $O^*(c^{\mu(\mathcal{F})})$ for a real number $c$, then we also
get a running time bound of $O^*(c^{L(\mathcal{F})})$ for this problem.
To obtain a running time bound in terms of the formula length $L(\mathcal{F})$, we consider the measure $\mu(\mathcal{F})$ and
show how much the measure $\mu(\mathcal{F})$ decreases in the branching operations of our algorithm and find the worst branching factor among all branching vectors.



\section{The Algorithm}
We will first introduce our algorithm and then analyze its running time bound by using the measure-and-conquer method.
Our algorithm consists of reduction operations and branching operations. When no reduction operations can be applied anymore, the algorithm will search for a solution by branching. We first introduce our reduction rules.
\subsection{Reduction Rules}
We have ten reduction rules. They are well-known and frequently used in the literature (see ~\cite{DBLP:conf/esa/Wahlstrom05,DBLP:conf/wads/ChenL09} for examples). So we may omit the proofs of the correctness of some rules.
We introduce the reduction rules in the order as stated and a reduction rule will be applied in our algorithm only when all previous reduction rules can not be applied on the instance.


\begin{rrule}[Elimination of duplicated literals]\label{rule-dup}
If a clause $C$ contains duplicated literals $z$, remove all but one $z$ in $C$.
\end{rrule}

\begin{rrule}[Elimination of subsumptions]\label{rule-subsump}
If there are two clauses $C$ and $D$ such that $C\subseteq D$, remove clause $D$.
\end{rrule}

\begin{rrule}[Elimination of tautology]\label{rule-tauto}
If a clause $C$ contains two opposite literals $z$ and $\overline{z}$, remove clause $C$.
\end{rrule}

\begin{rrule}[Elimination of $1$-clauses and pure literals]\label{rule-pure}
If there is a $1$-clause $\{x\}$ or a $(1^+, 0)$-literal $x$, assign $x=1$.
\end{rrule}

\textit{Davis-Putnam Resolution}, proposed in~\cite{DBLP:journals/jacm/DavisP60}, is a classic and frequently used technology for SAT.
Let $\mathcal{F}$ be a CNF-formula and $x$ be a variable in $\mathcal{F}$.
Assume that clauses containing literal $x$ are $xC_1,xC_2,...,xC_a$ and clauses containing literal $\overline{x}$ are $\overline{x}D_1, \overline{x}D_2, ..., \overline{x}D_b$. A \emph{Davis-Putnam resolution} on $x$ is to construct a new CNF-formula $DP_{x}(\mathcal{F})$ by the following method: initially $DP_{x}(\mathcal{F}) = \mathcal{F}$;
add new clauses $C_iD_j$ for each $1\leq i\leq a$ and  $1\leq j\leq b$; and remove $xC_1,xC_2,...,xC_a, \overline{x}D_1, \overline{x}D_2,...,\overline{x}D_b$ from the formula. It is known that
\begin{prop}[\cite{DBLP:journals/jacm/DavisP60}]
A CNF-formula $\mathcal{F}$ is satisfiable if and only if $DP_{x}(\mathcal{F})$ is satisfiable.
\end{prop}
In the resolution operation, each new clause $C_iD_j$ is called a \emph{resolvent}. A resolvent is \emph{trivial} if it contains both
a literal and the negation of it. Since trivial resolvents will always be satisfied, we can simply delete trivial resolvents from the instance directly. So when we do resolutions, we assume that all trivial resolvents will be deleted.


\begin{rrule}[Trivial resolution]\label{rule-trivial-resol}
If there is a variable $x$ with at most one non-trivial resolvent, then apply resolution on $x$.
\end{rrule}

\begin{rrule}[\cite{DBLP:conf/wads/ChenL09}]\label{rule-2cls-1neg}
If there are a $2$-clause $z_1z_2$ and a clause $C$ containing both $z_1$ and $\overline{z_2}$,
then  remove $\overline{z_2}$ from $C$.
\end{rrule}

\begin{rrule}\label{rule-1liter-neg}
If there are two clauses $z_1z_2C_1$ and $z_1\overline{z_2}C_2$, where literal $\overline{z_2}$ appears in no other clauses, then remove $z_1$ from clause $z_1z_2C_1$.
\end{rrule}
\begin{lemma}\label{proof-Rule7}
    Let  $\mathcal{F}$ be a CNF-formula and $\mathcal{F}'$ be the resulting formula after applying R-Rule~\ref{rule-1liter-neg} on $\mathcal{F}$. Then $\mathcal{F}$ is satisfiable if and only if $\mathcal{F}'$ is satisfiable.
\end{lemma}
\begin{proof}
Let $\mathcal{F}$ be the original formula and $\mathcal{F}'$ be the formula after replacing clause $z_1z_2C_1$ with clause $z_2C_1$
in $\mathcal{F}$. Clearly, if $\mathcal{F}'$ is satisfied then $\mathcal{F}$ is satisfied. We consider the other direction.

Assume that $\mathcal{F}$ is satisfied by an assignment $A$. We show that $\mathcal{F}'$ is also satisfied.
If  $z_2C_1$ is satisfied by assignment $A$, then $\mathcal{F}'$ is satisfied by assignment $A$.
Next, we assume assignment $A$ satisfies $z_1z_2C_1$ but not $z_2C_1$. Then in $A$, we have that $z_1=1$ and $z_2=0$.
 Since $\overline{z_2}$ is a $(1, 1^+)$-literal and $z_1\overline{z_2}C_2$ is the only clause containing $\overline{z_2}$,
 we know that all clauses will be satisfied if we replace $z_2=0$ with $z_2=1$ in $A$. Thus, $\mathcal{F}'$ is still satisfied.
\end{proof}

\begin{rrule}[\cite{DBLP:conf/wads/ChenL09}]\label{rule-2cls-2neg}
If there is a $2$-clause $z_1z_2$ and a clause $\overline{z_1}\overline{z_2}C$ such that literal $\overline{z_1}$ appears in no other clauses, remove the clause $z_1z_2$ from $\mathcal{F}$.
\end{rrule}

\begin{rrule}[\cite{DBLP:conf/wads/ChenL09}]\label{rule-link}
If there is a $2$-clause $z_1z_2$ such that either literal $z_1$ appears only in this clause or there is another $2$-clause $\overline{z_1}\overline{z_2}$, then replace $z_1$ with $\overline{z_2}$ in $\mathcal{F}$ and then apply R-Rule \ref{rule-tauto} as often as possible.
\end{rrule}


\begin{rrule}[\cite{DBLP:conf/wads/ChenL09}]\label{rule-back-resol}
If there are two clauses $CD_1$ and $CD_2$ such that $|D_1|, |D_2|\geq 1$ and $|C|\geq 2$, then remove $CD_1$ and $CD_2$ from $\mathcal{F}$, and add three new
clauses $xC$, $\overline{x}D_1$, and $\overline{x}D_2$, where $x$ is a new $3$-variable.
\end{rrule}

This is like the Davis-Putnam resolution in reverse and thus it is correct.

\begin{definition}[Reduced formulas]\label{def-reducedf}
A CNF-formula $\mathcal{F}$ is called \textit{reduced}, if none of the above reduction rules can be applied on it.
\end{definition}


Our algorithm will first iteratively apply above reduction rules in the order to get a reduced formula.
We will use $R(\mathcal{F})$ to denote the resulting reduced formula obtained from $\mathcal{F}$.
Next, we show some properties of reduced formulas.

\begin{lemma}\label{prop1}
In a reduced CNF-formula $\mathcal{F}$, all variables are $3^+$-variables.
\end{lemma}
\begin{proof}
If there is a $1$-variable, then R-Rule \ref{rule-pure} could be applied. For a $2$-variable in $\mathcal{F}$, if it is a $(2, 0)$-variable or $(0, 2)$-variable, then R-Rule \ref{rule-pure} could be applied; if it is a $(1, 1)$-variable, R-Rule \ref{rule-trivial-resol} could be applied.
\end{proof}

\begin{lemma}\label{prop2}
In a reduced CNF-formula $\mathcal{F}$, if there is a $2$-clause $xy$, then no other clause in $\mathcal{F}$ contains $xy$, $\overline{x}y$, or $x\overline{y}$.
\end{lemma}
\begin{proof}
If there is a clause containing $xy$, then R-Rule \ref{rule-back-resol} could be applied. If there is a clause containing $\overline{x}y$ or $x\overline{y}$, then R-Rule \ref{rule-2cls-1neg} could be applied.
\end{proof}



\begin{lemma}\label{prop4}
In a reduced CNF-formula $\mathcal{F}$, if there is a clause $xyC$, then
\begin{enumerate}[(i)]
    \item no other clause contains $xy$; \label{prop4-1}
    \item no other clause contains $\overline{x}y$ or $\overline{x}\overline{y}$ if $x$ is a $3$-variable. \label{prop4-2}
\end{enumerate}
\end{lemma}
\begin{proof}
(\ref{prop4-1}): If there is a clause containing $xy$, R-Rule \ref{rule-back-resol} can be applied.

(\ref{prop4-2}): Since $x$ is a $3$-variable and all $(1^+, 0)$-literals are reduced by R-Rule \ref{rule-pure}, $x$ is actually a $(1, 2)$-variable or $(2, 1)$-variable. If there is a clause containing $\overline{x}y$, R-Rule \ref{rule-1liter-neg} is applicable. If there is a clause containing $\overline{x}\overline{y}$, then there is only one non-trivial resolvent after resolving on $x$, which means R-Rule \ref{rule-trivial-resol} is applicable.
\end{proof}

\begin{lemma}\label{prop5}
In a reduced CNF-formula $\mathcal{F}$, if there is $(1, i)$-literal $x$ and $xC$ is the only clause containing $x$, then
\begin{enumerate}[(i)]
    \item $|C|\geq 2$; \label{prop5-1}
    \item all variables in $C$ are different from all variables in $N^{(2)}(\overline{x}, F)$, that is, if $y\in N^{(2)}(\overline{x}, F)$, then $y, \overline{y}\notin C$. \label{prop5-2}
\end{enumerate}
\end{lemma}
\begin{proof}
(\ref{prop5-1}): If $|C|=0$, then R-Rule \ref{rule-pure} could be applied; if $|C|=1$, which means $xC$ is a $2$-clause, then R-Rule \ref{rule-link} could be applied since $x$ is a $(1, i)$-literal.

(\ref{prop5-2}): Assume that $y$ is a literal in $N^{(2)}(\overline{x}, F)$, in other words, there is a $2$-clause $\overline{x}y$. Note that $x$ is a $(1, i)$-literal. If $y\in C$, then R-Rule \ref{rule-1liter-neg}
could be applied; if $\overline{y}\in C$, then R-Rule \ref{rule-2cls-2neg} could be applied.
\end{proof}

\subsection{Branching Rules and the Algorithm}
After getting a reduced formula, we will search for a solution by branching.
In a branching operation, we will generate two smaller CNF-formulas such that the original formula is satisfiable if and only if at least one of the two new formulas is satisfiable.
The two smaller formulas are generated by specifying the value of a set of literals in the original formula.

The simplest branching rule is that we pick up a variable or literal $x$ from $\mathcal{F}$ and branch into two branches $\mathcal{F}_{x=1}$ and $\mathcal{F}_{x=0}$,
where $\mathcal{F}_{x=1}$ and $\mathcal{F}_{x=0}$ are the formulas after assigning $x=1$ and $x=0$ in
$\mathcal{F}$, respectively. When the picked literal $x$ is a $(1,1^+)$-literal, we will apply a stronger branching.
Assume that $xC$ is the only clause containing $x$. Then we branch into two branches $\mathcal{F}_{x=1\And C=0}$ and $\mathcal{F}_{x=0}$,
where $\mathcal{F}_{x=1\And C=0}$ is the resulting formula after assigning 1 to $x$ and $0$ to all literals in $C$ in
$\mathcal{F}$.
The correctness of this branching operation is also easy to observe. Only when all literals in $C$ are assigned 0, we need to assign 1 to $x$.

\begin{algorithm*}[]\label{main-algorithm}
    \caption{SAT($\mathcal{F}$)}
    \KwIn{a CNF-formula $\mathcal{F}$}
    \KwOut{1 or 0 to indicate the satisfiability of $\mathcal{F}$}

   

    \textbf{Step 1.} If $\mathcal{F}=\emptyset$, return 1. If $\mathcal{F}$ contains an empty clause, return 0.\\
    \textbf{Step 2.} If $\mathcal{F}$ is not a reduced CNF-formula, iteratively apply the reduction rules to reduce it.\\
    \textbf{Step 3.} If there is a $d$-variable $x$ with $d\geq 6$, return SAT($\mathcal{F}_{x=1}$)$\vee$SAT($\mathcal{F}_{x=0}$).\\
    \textbf{Step 4.} If there is a $(1,4)$-literal $x$ (assume $xC$ is the only clause containing $x$), return SAT($\mathcal{F}_{x=1\And C=0}$)$\vee$SAT($\mathcal{F}_{x=0}$).\\
    \textbf{Step 5.} If there is a $5$-variable $x$ contained in a $2$-clause, return SAT($\mathcal{F}_{x=1}$)$\vee$SAT($\mathcal{F}_{x=0}$).\\
    \textbf{Step 6.} If there is a $5$-variable $x$ contained in a $4^+$-clause, return SAT($\mathcal{F}_{x=1}$)$\vee$SAT($\mathcal{F}_{x=0}$).\\
    \textbf{Step 7.} If there is a clause containing both a $5$-variable $x$ and a $4^-$-variable, return SAT($\mathcal{F}_{x=1}$)$\vee$SAT($\mathcal{F}_{x=0}$).\\
    \textbf{Step 8.} If there are still some 5-variables, then $\mathcal{F}=\mathcal{F}^* \wedge \mathcal{F}'$, where $\mathcal{F}^*$ is a 3-CNF with $var(\mathcal{F}^*)$ be the set of 5-variables in $\mathcal{F}$ and $var(\mathcal{F}^*)\cap var(\mathcal{F}') = \emptyset$.
    We return SAT($\mathcal{F}^*$) $\wedge$ SAT($\mathcal{F}'$) and solve $\mathcal{F}^*$ by using the $3$-SAT algorithm by Liu~\cite{DBLP:conf/icalp/Liu18}.\\
    \textbf{Step 9.} If  there is a $(1,3)$-literal $x$ (assume $xC$ is the only clause containing $x$), return SAT($\mathcal{F}_{x=1\And C=0}$)$\vee$SAT($\mathcal{F}_{x=0}$).\\
    \textbf{Step 10.} If  there is a $(2,2)$-literal $x$, return SAT($\mathcal{F}_{x=1}$)$\vee$SAT($\mathcal{F}_{x=0}$).\\
    \textbf{Step 11.} Apply the algorithm by Wahlstr{\"{o}}m~\cite{DBLP:conf/sat/Wahlstrom05} to solve the instance.
\end{algorithm*}

The main steps of our algorithm for the SAT problem are given in Algorithm~\ref{main-algorithm}. The algorithm will execute one step only when all previous steps can not be applied. In Step~2, the algorithm first reduces the formula by applying the reduction rules.
Step 3 will branch on a variable of degree $\geq 6$ if it exists. Steps 4-8 deal with 5-variables.
Note that if Steps 1-7 do not apply, then $\mathcal{F}$ can be written as $\mathcal{F}=\mathcal{F}^* \wedge \mathcal{F}'$, where $\mathcal{F}^*$ is a 3-CNF with $var(\mathcal{F}^*)$ be the set of 5-variables in $\mathcal{F}$ and $var(\mathcal{F}^*)\cap var(\mathcal{F}') = \emptyset$.
So we can do Step 8.
Steps 9-10 deal with 4-variables.
When the algorithm comes to the last step, all variables must have a degree of 3 and the algorithm deals with this special case.

We compare our algorithm with the previous algorithm by Chen and Liu~\cite{DBLP:conf/wads/ChenL09}.
We can see that they used a simple and uniform branching rule to deal with variables of degree at least 5 and used careful and complicated branching rules for 4-variables. Their bottlenecks contain one case
of branching on $(2,3)$-variables (or $(3,2)$-variables) and one case of dealing with 4-variables. To get further improvements, we carefully design and analyze the branching rules for 5-variables to avoid one previous bottleneck, and also refine the branching rules for 4-variables.



\section{Framework of the Analysis}
We use the measure-and-conquer method to analyze the running time bound of our algorithm, and adopt
 $\mu(\mathcal{F})$ defined in (\ref{measure}) as the measure to construct recurrence relations for our branching operations.
Before analyzing each detailed step of the algorithm, we first introduce the general framework of our analysis.

In each sub-branch of a branching operation, we assign value 1 or 0 to some literals and remove some clauses and literals. If we assign value 1 to a literal $x$ in the formula $\mathcal{F}$, then we will remove all clauses containing $x$ and all $\overline{x}$ literals from the clauses containing $\overline{x}$. The assignment and removing together are called an \emph{assignment operation}. We may assign values to more than one literal and we do assignment operations for each literal.
Let $S$ be a subset of literals. We use  $\mathcal{F}_{S=1}$ to denote the resulting formula after assigning 1 to each literal in $S$
and doing assignment operations. Note that $\mathcal{F}_{S=1}$ may not be a reduced formula and we will apply our reduction rules to reduce it. We use $\mathcal{F}'_{S=1}$ to denote the reduced formula obtained from $\mathcal{F}_{S=1}$, i.e.,
$\mathcal{F}'_{S=1}=R(\mathcal{F}_{S=1})$. We analyze how much we can reduce the measure in each branch by establishing some lower bounds for
\begin{equation*}
    \Delta_{S} = \mu(\mathcal{F}) - \mu(\mathcal{F}_{S=1}').
\end{equation*}

We also define
\begin{equation*}
    \xi_{S}^{(1)} = \mu(\mathcal{F}) - \mu(\mathcal{F}_{S=1});
\end{equation*}

\begin{equation*}
    \xi_{S}^{(2)} = \mu(\mathcal{F}_{S=1}) - \mu(\mathcal{F}_{S=1}').
\end{equation*}

Thus, $\Delta_{S} = \xi_{S}^{(1)} + \xi_{S}^{(2)}$.

In a branching operation, we will branch into two sub branches. Assume that the set of literals in $S_1$ are assigned the value in the first sub branch and the set of literals in $S_2$ are assigned the value in the second sub branch.  If we can show
$$ \min (\Delta_{S_1}, \Delta_{S_2}) \geq a ~~\text{and}~~ \Delta_{S_1}+ \Delta_{S_2} \geq b,$$
then we can always get a branching vector covered by one of
$$[a, b-a]~~~and~~~[b-a,a].$$
This technique will be frequently used in our analysis.

\subsection{Some Lower Bounds}

Next, we show some detailed lower bounds for $\Delta_{S}$ (as well as for $\Delta_{S_1}+\Delta_{S_2}$).  We first consider $\xi_{S}^{(1)}$ and $\xi_{S}^{(2)}$.


According to the assignment operation, we know that all variables of the literals in $S$ will be deleted in $\mathcal{F}_{S=1}$. So we have a
trivial bound
\begin{equation}\label{equ:dec-assign1}
    \xi_{S}^{(1)} \geq \sum_{v\in S}w_{deg(v)}.
\end{equation}

To get better bounds, we first define some notations.
For a literal $x$ in a reduced formula $\mathcal{F}$, we define:
\begin{itemize}
    \item $n_i(x)$: the number of $i$-variables whose literals appear in $N(x, \mathcal{F})$;
    \item $n'_i(x)$: the number of $i$-variables whose literals appear in $N^{(2)}(x, \mathcal{F})$;
    \item $n''_i(x)$: the number of $i$-variables whose literals appear in $N^{(3+)}(x, \mathcal{F})$.
\end{itemize}

Note that by the definition, we always have that $n_i(x)=n'_i(x)+n''_i(x)$.

Next, we give some lower bounds on $\xi_{S}^{(1)}$, $\xi_{S}^{(2)}$, and  $\Delta_{S_1}+\Delta_{S_2}$, which will be used to prove our main results.


\begin{lemma}\label{dec-assign2}
Assume that $\mathcal{F}$ is a reduced CNF-formula. Let $S = \{x\}$, where $x$ is a literal in $\mathcal{F}$. It holds that
\begin{equation}\label{equ:dec-assign2}
    \xi_{S}^{(1)} \geq w_{deg(x)} + \sum_{i\geq 3}n_i(x)\delta_i.
\end{equation}
\end{lemma}
\begin{proof}

After assigning value 1 to literal $x$, all clauses containing $x$ will be removed from $\mathcal{F}$, that is, all literals in $N(x, \mathcal{F})$ will be removed from $\mathcal{F}$.
By Lemma \ref{prop4}, we can know that all literals in $N(x, \mathcal{F})$ are unique.
For a variable $y$ in $N(x, \mathcal{F})$ (the variable of literal $y$ and $\overline{y}$ are the same, $y$), the degree of $y$ will decrease at most 2.
Moreover, if $y$ is a $3$-variable, by Lemma \ref{prop4}, we know that $y$ and $\overline{y}$ will not appear in $N(x, \mathcal{F})$ simultaneously since there is no other clause containing $x\overline{y}$. So the degree of $y$ will decrease by at most 1 if $y$ is a $3$-variable.

Let $t_{1, i}(x)$ and $t_{2, i}(x)$ denote the number of $i$-variables that appear once and twice in $N(x, \mathcal{F})$, respectively. We have $n_i(x) = t_{1, i}(x) + 2t_{2, i}(x)$ and $t_{2, 3}(x) = 0$. By the definition of $\xi_{S}^{(1)}$, we get that
\begin{align*}
    \xi_{S}^{(1)}
    & \geq w_{deg(x)} + (\sum_{3\leq i\leq d}{t_{1, i}(x)\delta_i}) + (\sum_{4\leq i\leq d}{t_{2, i}(x)(\delta_i+\delta_{i-1})})\\
    & \geq w_{deg(x)} + (\sum_{3\leq i\leq d}{t_{1, i}(x)\delta_i}) + (\sum_{4\leq i\leq d}{t_{2, i}(x)(\delta_i + \delta_i)})
    \qquad\qquad \text{by}~\delta_{i-1}\geq \delta_i \\
    & = w_{deg(x)} + (\sum_{3\leq i\leq d}{t_{1, i}(x)\delta_i}) + (\sum_{3\leq i\leq d}{2t_{2, i}(x)\delta_i})
    \qquad\qquad\quad \text{by}~ t_{2, 3}(x) = 0 \\
    & = w_{deg(x)} + \sum_{3\leq i\leq d}{(t_{1, i}(x) + 2t_{2, i}(x))\delta_i}
    \quad\quad\quad\quad \text{by}~ n_i(x) = t_{1, i}(x)+ 2t_{2, i}(x) \\
    & = w_{deg(x)} + \sum_{3\leq i\leq d}{n_i(x)\delta_i}.
\end{align*}
\end{proof}

\begin{lemma}\label{coro-assign2}
Assume that $\mathcal{F}$ is a reduced CNF-formula of degree $d$. Let $S = \{x\}$, where $x$ is a $(j, d-j)$-literal in $\mathcal{F}$. It holds that
\begin{equation}\label{equ:coro-assign2}
    \xi_{S}^{(1)} \geq w_d + j\delta_d.
\end{equation}
\end{lemma}
\begin{proof

By the condition, we can know that $deg(x) = j + d-j = d$ and $\sum_{3\leq i\leq d}n_i(x) \geq j$.
By Lemma \ref{dec-assign2}, we have
\begin{align*}
    \xi_{S}^{(1)}
    & \geq w_{deg(x)} + \sum_{3\leq i\leq d}n_i(x)\delta_i \\
    & \geq w_d + \sum_{3\leq i\leq d}n_i(x)\delta_d \\
    & = w_d + (\sum_{3\leq i\leq d}n_i(x))\delta_d \\
    & \geq w_d + j\delta_d
\end{align*}
\end{proof}

\begin{lemma}\label{dec-reduce}
Assume that $\mathcal{F}$ is a reduced CNF-formula of  degree $d$. Let $S = \{x\}$, where $x$ is a literal in $\mathcal{F}$. It holds that
\begin{equation}\label{equ:dec-reduce}
    \xi_{S}^{(2)}\geq n'_3(\overline{x})w_3 + \sum_{4\leq i\leq d}n'_i(\overline{x})w_{i-1}.
\end{equation}
\end{lemma}
\begin{proof

Recall that $\xi_{S}^{(2)}$ expresses how much the measure decrease after applying reduction rules on $\mathcal{F}_{S=1}$. All literals in $N(\overline{x}, \mathcal{F})$ will be assigned value 1 since R-Rule \ref{rule-pure} is applied. So we need to consider how the degree of each of variables in $N(\overline{x}, \mathcal{F})$ change in $\mathcal{F}_{S=1}$.
By Lemma \ref{prop2}, for a literal $y\in N^{(2)}(\overline{x}, \mathcal{F})$, we can know that there is no other clause containing $xy$. So if variable $y$ is an $i$-variable in $\mathcal{F}$, then the degree of $y$ in $\mathcal{F}_{S=1}$ is at least $i-1$.
Moreover, for a literal $y\in N^{(2)}(x, \mathcal{F})$ such that $y$ is a $3$-variable, we can know that there is no other clause containing $xy$ or $x\overline{y}$ with Lemma \ref{prop4}, which means $y$ would still be a $3$-variable in $\mathcal{F}_{S=1}$.
Since all variables in $N(\overline{x}, \mathcal{F})$ would not appear in $\mathcal{F}_{S=1}'$ and these variables are distinct from each other by Lemma \ref{prop2}, the lemma holds by the definition of $\xi_{S}^{(2)}$.
\end{proof}

\begin{lemma}\label{dec-sum}
Assume that $\mathcal{F}$ is a reduced CNF-formula of degree $d$. Let $S_1 = \{x\}$ and $S_2 = \{\overline{x}\}$, where the corresponding variable of $x$ is a $d$-variable in $\mathcal{F}$. It holds that
\begin{equation}\label{equ:dec-sum}
\begin{aligned}
    \Delta_{S_1}+\Delta_{S_2}
    &\geq 2w_d + 2d\delta_d + (n'_3(x)+n'_3(\overline{x}))(2w_3-2\delta_d)\\
    &~~~~+ \sum_{4\leq i\leq d}{(n'_i(x)+n'_i(\overline{x}))(w_i-2\delta_d)}.
\end{aligned}
\end{equation}
\end{lemma}
\begin{proof

We can get that
\begin{align*}
    &\xi_{S_1}^{(1)} \geq w_d + \sum_{3\leq i\leq d}n_i(x)\delta_i.
    &\text{by Lemma \ref{dec-assign2} and } deg(x)=d \\
    &\xi_{S_1}^{(2)}\geq n'_3(\overline{x})w_3 + \sum_{4\leq i\leq d}n'_i(\overline{x})w_{i-1}.
    &\text{by Lemma \ref{dec-reduce}}
\end{align*}
And we can get bounds on $\xi_{S_2}^{(1)}$ and $\xi_{S_2}^{(2)}$ by the same way.
So we have that
\begin{equation}\label{aux-bound-1}
\begin{aligned}
    \Delta_{S_1} &= \xi_{S_1}^{(1)} + \xi_{S_1}^{(2)} \geq w_d + (\sum_{3\leq i\leq d}n_i(x)\delta_i) + n'_3(\overline{x})w_3 + \sum_{4\leq i\leq d}n'_i(\overline{x})w_{i-1}. \\
    \Delta_{S_2} &= \xi_{S_2}^{(1)} + \xi_{S_2}^{(2)} \geq w_d + (\sum_{3\leq i\leq d}n_i(\overline{x})\delta_i) + n'_3(x)w_3 + \sum_{4\leq i\leq d}n'_i(x)w_{i-1}.
\end{aligned}
\end{equation}
By the definition of $n_i$ and $n_i(\overline{x})$, we have
\begin{equation}\label{eq-n}
    n_i(x)=n'_i(x)+n''_i(x),n_i(\overline{x})=n'_i(\overline{x})+n''_i(\overline{x}).
\end{equation}
And note that $\sum_{3\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))$ is exactly the number of $2$-clauses containing $x$ or $\overline{x}$, so we have
\begin{equation}\label{ineq-n}
    \sum_{3\leq i\leq d}(n''_i(x)+n''_i(\overline{x}))\geq 2(d-\sum_{3\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))).
\end{equation}
Now we are ready to proof the lemma:
\begin{align*}
    \Delta_{S_1}+\Delta_{S_2}
    &\geq w_d + (\sum_{3\leq i\leq d}n_i(x)\delta_i) + n'_3(\overline{x})w_3 + \sum_{4\leq i\leq d}n'_i(\overline{x})w_{i-1} \\
    & \quad + w_d + (\sum_{3\leq i\leq d}n_i(\overline{x})\delta_i) + n'_3(x)w_3 + \sum_{4\leq i\leq d}n'_i(x)w_{i-1}
    ~~~~ \text{by (\ref{aux-bound-1})} 
    \\
    & = 2w_d + (n'_3(x)+n'_3(\overline{x}))w_3 + \sum_{4\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))w_{i-1} \\
    & \quad + \sum_{3\leq i\leq d}(n_i(x)+n_i(\overline{x}))\delta_i
    \\
    & = 2w_d + (n'_3(x)+n'_3(\overline{x}))w_3 + \sum_{4\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))w_{i-1} \\
    & \quad + \sum_{3\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))\delta_i + \sum_{3\leq i\leq d}(n''_i(x)+n''_i(\overline{x}))\delta_i
    ~~~~~~ \text{by (\ref{eq-n})} 
    \\
    & \geq 2w_d + (n'_3(x)+n'_3(\overline{x}))w_3 + \sum_{4\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))w_{i-1} \\
    & \quad + \sum_{3\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))\delta_i + (\sum_{3\leq i\leq d}(n''_i(x)+n''_i(\overline{x})))\delta_d
    \\
    & \geq 2w_d + (n'_3(x)+n'_3(\overline{x}))w_3 + \sum_{4\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))w_{i-1} \\
    & \quad + \sum_{3\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))\delta_i + 2(d-\sum_{3\leq i\leq d}(n'_i(x)+n'_i(\overline{x})))\delta_d
    ~~~ \text{by (\ref{ineq-n})} 
    \\
    & = 2w_d + 2d\delta_d + (n'_3(x)+n'_3(\overline{x}))w_3 + \sum_{4\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))w_{i-1} \\
    & \quad + \sum_{3\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))(\delta_i-2\delta_d)
    \\
    & = 2w_d + 2d\delta_d + (n'_3(x)+n'_3(\overline{x}))(w_3+\delta_3-2\delta_d) \\
    & \quad + \sum_{4\leq i\leq d}(n'_i(x)+n'_i(\overline{x}))(w_{i-1}+\delta_i-2\delta_d)
    \\
    & = 2w_d + 2d\delta_d + (n'_3(x)+n'_3(\overline{x}))(2w_3-2\delta_d)\\
    & \quad + \sum_{4\leq i\leq d}{(n'_i(x)+n'_i(\overline{x}))(w_i-2\delta_d)}.
    \qquad\qquad\qquad\qquad \text{by (\ref{eq-w3-d3-d4})}
\end{align*}
\end{proof}

\begin{lemma}\label{dec-1ltr}
Assume that $\mathcal{F}$ is a reduced CNF-formula of degree $d$. Let $x$ be a $(1, d-1)$-literal and $xC$ be the
only clause containing $x$  in $\mathcal{F}$. Let $S=\{x\}\cup \overline{C}$. It holds that
\begin{equation}\label{equ:dec-1ltr}
    \Delta_{S}\geq w_d+2w_3+\sum_{3\leq i\leq d}{n'_i(\overline{x})w_i}.
\end{equation}
\end{lemma}
\begin{proof}

By Lemma \ref{prop5}, we can know that $|C|\geq 2$ and all variables in $C$ and $N^{(2)}(\overline{x}, \mathcal{F})$ are different. So after assigning value 1 to all literals in $S$, all $2$-clauses containing $\overline{x}$ in $\mathcal{F}$ would become $1$-clauses in $\mathcal{F}_{S=1}$ and the degree of each variable in these $1$-clauses would not change after assigning operation. Then, by applying R-Rule \ref{rule-pure}, all variables in these $1$-clauses get assignments. In conclusion, all variables in $C$ and $N^{(2)}(\overline{x}, \mathcal{F})$ would not appear in $\mathcal{F}_{S=1}'$. By the definition of $\Delta_{S}$, we have
\begin{align*}
    \Delta_{S}
    & \geq \sum_{v\in S}w_{deg(v)} + \sum_{3\leq i\leq d}n'_i(\overline{x})w_i\\
    & \geq w_d+(|S|-1)w_3 + \sum_{3\leq i\leq d}n'_i(\overline{x})w_i\\
    & = w_d+|C|w_3 + \sum_{3\leq i\leq d}n'_i(\overline{x})w_i\\
    & \geq w_d+2w_3 + \sum_{3\leq i\leq d}{n'_i(\overline{x})w_i}.
\end{align*}

\end{proof}

\begin{lemma}\label{dec-1ltr-sum}
Assume that $\mathcal{F}$ is a reduced CNF-formula of degree $d$. Let $x$ be a $(1, d-1)$-literal and $xC$ be the
only clause containing $x$ in $\mathcal{F}$. Let $S_1=\{x\}\cup \overline{C}$ and $S_2=\{\overline{x}\}$. It holds that
\begin{equation}\label{equ:dec-1ltr-sum}
    \Delta_{S_1}+\Delta_{S_2}\geq 2w_d+2w_3+2(d-1)\delta_d.
\end{equation}
\end{lemma}
\begin{proof}

We can get that
\begin{equation}\label{aux-bound-2}
\begin{aligned}
    &\Delta_{S_1}\geq w_d+2w_3+\sum_{3\leq i\leq d}{n'_i(\overline{x})w_i}.
    &\text{by Lemma \ref{dec-1ltr}}
    \\
    &\Delta_{S_2}\geq w_d+\sum_{3\leq i\leq d}n_i(\overline{x})\delta_i.
    &\text{by Lemma \ref{dec-assign2} and $deg(x)=d$}
\end{aligned}
\end{equation}
Since $\overline{x}$ is a $(d-1,1)$-literal, the number of literals in $N^{(3+)}(\overline{x}, \mathcal{F})$, namely $\sum_{3\leq i\leq d}n''_i(\overline{x})$, is at least $2((d-1)-\sum_{3\leq i\leq d}n'_i(\overline{x}))$. We can know that
\begin{equation}\label{ineq-neg-ni}
\begin{aligned}
    \sum_{3\leq i\leq d}{n_i(\overline{x})}
    & = \sum_{3\leq i\leq d}{n'_i(\overline{x})} + \sum_{3\leq i\leq d}{n''_i(\overline{x})}
    & \text{by (\ref{eq-n})}
    \\
    & \geq \sum_{3\leq i\leq d}{n'_i(\overline{x})} + 2((d-1)-\sum_{3\leq i\leq d}n'_i(\overline{x}))
    \\
    & = 2(d-1) - \sum_{3\leq i\leq d}n'_i(\overline{x}).
\end{aligned}
\end{equation}
So we have
\begin{align*}
    \Delta_{S_1}+\Delta_{S_2}
    & \geq w_d+2w_3+(\sum_{3\leq i\leq d}{n'_i(\overline{x})w_i}) + w_d+\sum_{3\leq i\leq d}n_i(\overline{x})\delta_i~~~~~\text{by (\ref{aux-bound-2})}
    \\
    & \geq 2w_d+2w_3 + (\sum_{3\leq i\leq d}{n'_i(\overline{x})w_i}) + (\sum_{3\leq i\leq d}n_i(\overline{x}))\delta_d
    \\
    & \geq 2w_d+2w_3 + (\sum_{3\leq i\leq d}{n'_i(\overline{x})w_i})\\
    &~~~~ + (2(d-1) - \sum_{3\leq i\leq d}n'_i(\overline{x}))\delta_d  \qquad\qquad\qquad\qquad\qquad \text{by (\ref{ineq-neg-ni})}
    \\
    & = 2w_d+2w_3+2(d-1)\delta_d+\sum_{3\leq i\leq d}n'_i(\overline{x})(w_i-\delta_d)
    \\
    & \geq 2w_d+2w_3+2(d-1)\delta_d.
\end{align*}
\end{proof}

\begin{lemma}\label{dec-sum-5d3c}
Assume that $\mathcal{F}$ is a reduced CNF-formula of $d=5$. Let $S_1=\{x\}$ and $S_2=\{\overline{x}\}$, where the corresponding variable of $x$ is a $5$-variable in $\mathcal{F}$. If all clauses containing $x$ or $\overline{x}$ are $3^+$-clauses, it holds that
\begin{equation}\label{equ:dec-sum-5d3c}
\begin{aligned}
    \Delta_{S_1}+\Delta_{S_2}
    &\geq 2w_5+(\sum_{3\leq i\leq 5}{(n_i(x)+n_i(\overline{x}))})\delta_5\\
    &~~~~+(\sum_{3\leq i\leq 4}{(n_i(x)+n_i(\overline{x}))})(w_3-\delta_5).
\end{aligned}
\end{equation}
\end{lemma}


\begin{proof}

By Lemma \ref{dec-assign2} and $deg(x)=d=5$, we can get that
\begin{equation}\label{aux-bound-3}
\begin{aligned}
    \Delta_{S_1}\geq w_5 + \sum_{3\leq i\leq 5}n_i(x)\delta_i.\\
    \Delta_{S_2}\geq w_5 + \sum_{3\leq i\leq 5}n_i(\overline{x})\delta_i.
\end{aligned}
\end{equation}
So we have
\begin{align*}
    \Delta_{S_1}+\Delta_{S_2}
    & \geq w_5 + \sum_{3\leq i\leq 5}n_i(x)\delta_i + w_5 + \sum_{3\leq i\leq 5}n_i(\overline{x})\delta_i
    ~~~~~~~~~~ \text{by (\ref{aux-bound-3})}
    \\
    & = 2w_5 + (n_3(x)+n_3(\overline{x}))\delta_3 + (n_4(x)+n_4(\overline{x}))\delta_4 + (n_5(x)+n_5(\overline{x}))\delta_5
    \\
    & = 2w_5 + (\sum_{3\leq i\leq 5}{(n_i(x)+n_i(\overline{x}))}-\sum_{3\leq i\leq 4}{(n_i(x)+n_i(\overline{x}))})\delta_5\\
    & \quad + (\sum_{3\leq i\leq 4}{(n_i(x)+n_i(\overline{x}))})w_3
    ~~~~~~~~~~~~~~~~~~~~~~~~~~ \text{by (\ref{eq-w3-d3-d4})}
    \\
    & = 2w_5+(\sum_{3\leq i\leq 5}{(n_i(x)+n_i(\overline{x}))})\delta_5+(\sum_{3\leq i\leq 4}{(n_i(x)+n_i(\overline{x}))})(w_3-\delta_5).
\end{align*}
\end{proof}


\section{Step Analysis}
Equipped with the above lower bounds, we are ready to analyze the branching vector of each step in the algorithm.

\subsection{Step 2}
In this step, we do not branch and only apply reduction rules to reduce the formula.
However, it is still important to show that the measure will never increase when applying reduction rules, and reduction operations use only polynomial time.


\begin{lemma}\label{reduction-measure}
For any CNF-formula $\mathcal{F}$, it holds that
$$\mu(R(\mathcal{F}))\leq \mu(\mathcal{F}).$$
\end{lemma}
\begin{proof

It suffices to verify that each reduction rule would not increase the measure of the formula.

R-Rule 1-8 simply remove some literals, which would not increase the measure of the formula.

Next, we consider R-Rule \ref{rule-link} and \ref{rule-back-resol}. Note that now
R-Rule \ref{rule-pure} and \ref{rule-trivial-resol} are not applicable, and then all variables in $\mathcal{F}$ are $3^+$-variables.
The reason is below.
If there is a $1$-variable, we could apply R-Rule \ref{rule-pure}. For a $2$-variable in $\mathcal{F}$, if it is a $(2, 0)$-variable or $(0, 2)$-variable, R-Rule \ref{rule-pure} would be applicable; if it is a $(1, 1)$-variable, R-Rule \ref{rule-trivial-resol} would be applicable.

For R-Rule \ref{rule-link}, without loss of generalization, we assume $z_1$ is an $i$-variable and $z_2$ is a $j$-variable such that $3\leq i\leq j$. After applying this rule, $z_2$ will become an $i+j-2$-variable since we replace $z_1$ with $\overline{z_2}$ and clause $z_1z_2$ is removed by R-Rule \ref{rule-tauto}. Next, we show that $\mu(R(\mathcal{F}))-\mu(\mathcal{F})=w_{i+j-2}-w_i-w_j\leq 0$ holds. 

By (\ref{weight1}), (\ref{weight2}) and (\ref{eq-w3-d3-d4}), we can know that: if $i=3$, then $$w_{3+j-2}-w_3-w_j=\delta_{j+1}-w_3\leq \delta_4-w_3 = 0;$$ 
if $i=4$, then $$w_{4+j-2}-w_4-w_j=\delta_{j+2}+\delta_{j+1}-w_4\leq \delta_6+\delta_5-w_4<0;$$ 
if $i\geq 5$, then $$w_{i+j-2}-w_i-w_j=(i+j-2)-i-j=-2<0.$$

For R-Rule \ref{rule-back-resol},  two clauses $CD_1$ and $CD_2$ in $\mathcal{F}$ are replaced with three clauses $xC, \overline{x}D_1$ and $\overline{x}D_2$. We introduce a $3$-variable $x$ and also decrease the degree of each variable in $C$ by 1. The introduction of $x$ increases the measure of the formula by $w_3$. On the other hand, since all variables are $3^+$-variable in $\mathcal{F}$ and $|C|\geq 2$, the degree decreasing for the variables in $C$
contributes the measure decreasing of at least $2\min\{\delta_i|i\geq 3\}=2$. Since $w_3<2$, we know that $$\mu(R(\mathcal{F}))-\mu(\mathcal{F})=w_3-2\min\{\delta_i|i\geq 3\} = w_3-2 < 2-2=0.$$
\end{proof}

\begin{lemma}\label{Rpolytime}
For any CNF-formula $\mathcal{F}$,
we can apply the reduction rules in polynomial time to transfer it to $R(\mathcal{F})$.
\end{lemma}
\begin{proof

Each application of any one of the first eight reduction rules removes some literal from the formula and then it decreases $L(\mathcal{F})$ at least by 1.
For R-Rule \ref{rule-link}, after replacing $z_1$ with $\overline{z_2}$, the clause $z_1z_2$ will be removed by R-Rule \ref{rule-tauto}. So each application of it decreases $L(\mathcal{F})$ by at least 2.

It is easy to see that each application of R-Rule \ref{rule-back-resol} increases $L(\mathcal{F})$ by at most 1.
In the proof of Lemma \ref{reduction-measure}, we have shown that  the measure $\mu(\mathcal{F})$ decreases at least by $2-w_3$ in this step. Since $w_3$ is a constant less than $2$, let $w_3=2-\epsilon$ for a constant $\epsilon$, then $\mu(\mathcal{F})$ decreases by at least $\epsilon$ after applying R-Rule \ref{rule-back-resol}.

In order to make the proof clear, we define a new measure $M(\mathcal{F})=L(\mathcal{F})+2\mu(\mathcal{F})/\epsilon$.
It is easy to see that  $M(\mathcal{F})$ is bounded by a polynomial of $L(\mathcal{F})$.
For R-Rule 1-9, it decreases $M(\mathcal{F})$ by at least 1. For R-Rule \ref{rule-back-resol}, it increases $M(\mathcal{F})$ by at most 1. Assume the resulted CNF-formula after applying R-Rule \ref{rule-back-resol} is $\mathcal{F}'$. It holds that $L(\mathcal{F})-L(\mathcal{F}')\geq -1$ and $\mu(\mathcal{F})-\mu(\mathcal{F}')\geq \epsilon$. So $$M(\mathcal{F})-M(\mathcal{F}')=L(\mathcal{F})-L(\mathcal{F}')+2(\mu(\mathcal{F})-\mu(\mathcal{F}'))/\epsilon \geq -1+2=1.$$ Since each reduction rule decreases $M(\mathcal{F})$ at least by 1, it must stop in polynomial time if we iteratively apply the reduction rules.
\end{proof}



\subsection{Step 3}\label{subsec-step3}
In this step, we branch on a variable $x$ of degree at least 6. The two sub-branches are:  $S_1=\{x\}$;  $S_2=\{\overline{x}\}$. We have the following result:
\begin{lemma}
    The branching vector generated by Step 3 is covered
    \begin{equation}\label{vec-step3}
        [w_6+\delta_6, w_6+11\delta_6]~\text{or}~[w_6+11\delta_6, w_6+\delta_6].
    \end{equation}
\end{lemma}
\begin{proof}

Since R-Rule \ref{rule-pure} is not applicable, both $x$ and $\overline{x}$ are $(1^+,1^+)$-literals. By the condition of this case, we have $d\geq 6$ and $\delta_d=\delta_6$ by (\ref{weight1}).

By Lemma \ref{coro-assign2}, we can get that $\Delta_{S_1}\geq \xi_{S_1}^{(1)} \geq w_d + j\delta_d \geq w_6 + \delta_6$ since $x$ is a $(j, d-j)$-literal with $j\geq 1$. Also, we can get $\Delta_{S_2}\geq w_6+\delta_6$ by the same method.

By Lemma \ref{dec-sum}, $w_3>\delta_d$ and $w_i>2\delta_d$ for $4\leq i\leq d$, we have that
\begin{align*}
    \Delta_{S_1}+\Delta_{S_2}
    & \geq 2w_d + 2d\delta_d + (n'_3(x)+n'_3(\overline{x})) (2w_3-2\delta_d) \\
    & ~~~~ +\sum_{4\leq i\leq d}{(n'_i(x)+n'_i(\overline{x}))(w_i-2\delta_d)} \\
    & \geq 2w_6 + 12\delta_d.
\end{align*}


With $\min(\Delta_{S_1},\Delta_{S_2})\geq w_6+\delta_6$ and $\Delta_{S_1}+\Delta_{S_2}\geq 2w_6+12\delta_6$, we can know that the branching vector of this case is covered by
$$
[w_6+\delta_6, w_6+11\delta_6] ~~\mbox{or}~~ [w_6+11\delta_6, w_6+\delta_6].
$$
\end{proof}

\subsection{Step 4}\label{subsec-step4}
In this step, the algorithm will consider a $(1,4)$-literal $x$. Assume that $xC$ is the only clause containing $x$. The two sub-branches are: $S_1=\{x\}\cup \overline{C}$; $S_2=\{\overline{x}\}$. We have the following result:
\begin{lemma}
    The branching vector generated by step 4 is covered by
    \begin{equation}\label{vec-step4}
        [w_5+2w_3, w_5+8\delta_5]~\text{or}~[w_5+8\delta_5, w_5+2w_3].
    \end{equation}
\end{lemma}
\begin{proof}

By Lemma \ref{dec-1ltr}, we get that $\Delta_{S_1}\geq w_d+2w_3+\sum_{3\leq i\leq d}{n'_i(\overline{x})w_i}\geq w_5+2w_3$. By Lemma \ref{coro-assign2}, we have that $\Delta_{S_2}\geq \xi_{S_2}^{(1)} \geq w_d + j\delta_d= w_5+4\delta_5$ since $\overline{x}$ is a $(4, 1)$-literal.

By Lemma \ref{dec-1ltr-sum}, we can get that $\Delta_{S_1}+\Delta_{S_2}\geq 2w_d+2w_3+2(d-1)\delta_d= 2w_5+2w_3+8\delta_5$.

 Since $w_3<2$ and $w_5=5$ by (\ref{weight1}), we have $2w_5> 5w_3$, i.e., $2w_5-4w_3> w_3$. Since $w_4=2w_3$ by (\ref{weight2}), we have $2w_5-2w_4> w_3$, which implies that $2\delta_5> w_3$. So $\min(\Delta_{S_1}, \Delta_{S_2})\geq w_5+2w_3$. Since $\Delta_{S_1}+\Delta_{S_2}\geq 2w_5+2w_3+8\delta_5$, we know that the branching vector of this case is covered by
$$
[w_5+2w_3, w_5+8\delta_5] ~~\mbox{or}~~ [w_5+8\delta_5, w_5+2w_3].
$$
\end{proof}

\subsection{Step 5}\label{subsec-step5}
In this step, we branch on a $5$-variable $x$ such that either $x$ or $\overline{x}$ is in a $2$-clause. The two sub-branches are:  $S_1=\{x\}$;  $S_2=\{\overline{x}\}$. We have the following result:
\begin{lemma}
    The branching vector generated by step 5 is covered by one of
    \begin{align*}\label{vec-step5}
        [w_5+2\delta_5, w_5+4w_3+4\delta_5]\text{,}~[w_5+4w_3+4\delta_5, w_5+2\delta_5]\text{,}\\
        [w_5+3\delta_5, w_5+2w_3+5\delta_5],~\text{and}~[w_5+2w_3+5\delta_5, w_5+3\delta_5].
    \end{align*}
\end{lemma}
\begin{proof}

We will consider two subcases:

\textbf{Case 1.} There are at least two 2-clause containing literal $x$ or $\overline{x}$. Now it holds that $\sum_{3\leq i\leq d}n'_i(x)+n'_i(\overline{x})\geq 2$. By Lemma \ref{coro-assign2}, we get that $\Delta_{S_1}\geq \xi_{S_1}^{(1)} \geq w_d + j\delta_d\geq w_5+2\delta_5$ since $x$ is a $(2,3)$-literal or $(3,2)$-literal. In a similar way,
 we can get that $\Delta_{S_2}\geq w_5+2\delta_5$.

 By Lemma \ref{dec-sum}, $w_4,w_5\geq 2w_3$, and $\sum_{3\leq i\leq 5}n'_i(x)+n'_i(\overline{x})\geq 2$, we have that
\begin{align*}
\Delta_{S_1}+\Delta_{S_2}&\geq 2w_d + 2d\delta_d + (n'_3(x)+n'_3(\overline{x}))(2w_3-2\delta_d)\\
 &~~~~ + \sum_{4\leq i\leq d}{(n'_i(x)+n'_i(\overline{x}))(w_i-2\delta_d)}\\
 &\geq 2w_5 + 10\delta_5 + \sum_{3\leq i\leq 5}{(n'_i(x)+n'_i(\overline{x}))(2w_3-2\delta_5)}\\
 &\geq 2w_5+10\delta_5+2(w_3-2\delta_5)\\
 &\geq 2w_5+4w_3+6\delta_5.
\end{align*}

  By $\min(\Delta_{S_1}, \Delta_{S_2})\geq w_5+2\delta_5$ and $\Delta_{S_1}+\Delta_{S_2}\geq 2w_5+4w_3+6\delta_5$, we  know that the branching vector of this case is covered by
  $$[w_5+2\delta_5, w_5+4w_3+4\delta_5] ~~\mbox{or}~~ [w_5+4w_3+4\delta_5, w_5+2\delta_5].$$

\textbf{Case 2.} There is only one $2$-clause containing literal $x$ or $\overline{x}$. Note that $\sum_{3\leq i\leq d}n'_i(x)+n'_i(\overline{x})=1$. For literal $x$, it is contained in at least two clauses and at most one of them is $2$-clause. So $\sum_{3\leq i\leq d}n_i(x)\geq 3$ holds.

By Lemma \ref{dec-assign2}, we get that $\Delta_{S_1}\geq \xi_{S_1}^{(1)} \geq w_5 + \sum_{3\leq i\leq d}n_i(x)\delta_i\geq w_5 + (\sum_{3\leq i\leq d}n_i(x))\delta_5\geq w_5+3\delta_5$.
Similarly, we also can get that $\Delta_{S_2}\geq w_5+3\delta_5$.
By Lemma \ref{dec-sum}, $w_4,w_5\geq 2w_3$ and $\sum_{3\leq i\leq d}n'_i(x)+n'_i(\overline{x})= 1$, we get that
\begin{align*}
\Delta_{S_1}+\Delta_{S_2}
&\geq 2w_d + 2d\delta_d + (n'_3(x)+n'_3(\overline{x}))(2w_3-2\delta_d) \\
&~~~~+\sum_{4\leq i\leq d}{(n'_i(x)+n'_i(\overline{x}))(w_i-2\delta_d)}\\
&\geq 2w_5 + 10\delta_5 + \sum_{3\leq i\leq 5}{(n'_i(x)+n'_i(\overline{x}))(2w_3-2\delta_5)}\\
&\geq 2w_5+10\delta_5+(2w_3-2\delta_5) \\
&\geq 2w_5+2w_3+8\delta_5.
\end{align*}


Since $\min(\Delta_{S_1},\Delta_{S_2})\geq w_5+3\delta_5$ and $\Delta_{S_1}+\Delta_{S_2}\geq 2w_5+2w_3+8\delta_5$, we know that the branching vector of this subcase is covered by
$$
[w_5+3\delta_5, w_5+2w_3+5\delta_5] ~~\mbox{or}~~ [w_5+2w_3+5\delta_5, w_5+3\delta_5].
$$

These two cases complete the proof.
\end{proof}


\subsection{Step 6}\label{subsec-step6}
In this step, all clauses containing a $5$-variable are $3^+$-clauses now. We branch on a $5$-variable $x$ contained in a $4^+$-clause. The two sub-branches are: $S_1=\{x\}$; $S_2=\{\overline{x}\}$. We have the following result:
\begin{lemma}
    The branching vector generated by step 6 is covered by
    \begin{equation}\label{vec-step6}
        [w_5+4\delta_5, w_5+7\delta_5]~\text{or}~[w_5+7\delta_5, w_5+4\delta_5].
    \end{equation}
\end{lemma}
\begin{proof}

Literal $x$ is contained in at least two $3^+$-clauses. So $\sum_{3\leq i\leq d}n_i(x)\geq 4$ holds. By Lemma \ref{dec-assign2}, we get that $\Delta_{S_1}\geq \xi_{S_1}^{(1)} \geq w_5 + (\sum_{3\leq i\leq d}n_i(x))\delta_d\geq w_5+4\delta_5$. Similarly, we get that $\Delta_{S_2}\geq w_5+4\delta_5$.

Let $m_4$ be the number of $4^+$-clauses containing $x$. Since $m_4\geq 1$, we have that $$\sum_{3\leq i\leq 5}n_i(x)+n'_i(x)\geq 2(5-m_4)+3m_4\geq 10+m_4\geq 11.$$
By Lemma \ref{dec-sum-5d3c} and $w_3\geq \delta_5$, We get that
\begin{align*}
\Delta_{S_1}+\Delta_{S_2}
&\geq 2w_5+(\sum_{3\leq i\leq 5}{(n_i(x)+n_i(\overline{x}))})\delta_5\\
&~~~~+(\sum_{3\leq i\leq 4}{(n_i(x)+n_i(\overline{x}))})(w_3-\delta_5)\\
&\geq 2w_5+11\delta_5.
\end{align*}

Since $\min(\Delta_{S_1}, \Delta_{S_2})\geq w_5+4\delta_5$ and $\Delta_{S_1}+\Delta_{S_2}\geq 2w_5+11\delta_5$, we know that the branching vector of this case is covered by
$$
[w_5+4\delta_5, w_5+7\delta_5]~~\mbox{or}~~[w_5+7\delta_5, w_5+4\delta_5].
$$
\end{proof}

\subsection{Step 7}\label{subsec-step7}
In Step 7, all clauses containing a $5$-variable are $3$-clauses. We branch on a $5$-variable $x$
whose literal and a literal of a $4^-$-variable are in the same clause. The two sub-branches are: $S_1=\{x\}$; $S_2=\{\overline{x}\}$. We have that
\begin{lemma}
    The branching vector generated by step 7 is covered by
    \begin{equation}\label{vec-step7}
        [w_5+4\delta_5, w_5+w_3+5\delta_5]~\text{or}~[w_5+w_3+5\delta_5, w_5+4\delta_5].
    \end{equation}
\end{lemma}
\begin{proof}
There is at least one $4^-$-variable whose literal is in $N(x, \mathcal{F})\cup N(\overline{x}, \mathcal{F})$. So it holds that $\sum_{3\leq i\leq 4}(n_i(x)+n_i(\overline{x}))\geq 1$.

For literal $x$, it is contained in at least two $3$-clauses, which means that $\sum_{3\leq i\leq d}n_i(x)\geq 4$ holds. By Lemma \ref{dec-assign2}, we get that $\Delta_{S_1}\geq \xi_{S_1}^{(1)} \geq w_5 + \sum_{3\leq i\leq 5}n_i(x)\delta_i\geq w_5 + (\sum_{3\leq i\leq d}n_i(x))\delta_5=w_5 + 4\delta_5$. Similarly, we can get that $\Delta_{S_2}\geq w_5+4\delta_5$.

By Lemma \ref{dec-sum-5d3c} and $\sum_{3\leq i\leq 4}n_i(x)+n_i(\overline{x})\geq 1$, we get that
\begin{align*}
\Delta_{S_1}+\Delta_{S_2}
&\geq 2w_5+(\sum_{3\leq i\leq 5}{(n_i(x)+n_i(\overline{x}))})\delta_5\\
&~~~~+(\sum_{3\leq i\leq 4}{(n_i(x)+n_i(\overline{x}))})(w_3-\delta_5)\\
&\geq 2w_5+w_3+9\delta_5.
\end{align*}

Since $\min(\Delta_{S_1},\Delta_{S_2})\geq w_5+4\delta_5$ and $\Delta_{S_1}+\Delta_{S_2}\geq 2w_5+2w_3+8\delta_5$, we know that the branching vector is covered by
$$
[w_5+4\delta_5, w_5+w_3+5\delta_5]~~\mbox{or}~~[w_5+w_3+5\delta_5, w_5+4\delta_5].
$$
\end{proof}

\subsection{Step 8}
In Step 8, the literals of all $5$-variables form a $3$-SAT instance $\mathcal{F}^*$. We apply the $O^*(1.3279^n)$-time algorithm in~\cite{DBLP:conf/icalp/Liu18} for 3-SAT to solve our problem, where $n$ is the number of variables in the instance. Since $w_5=5$, we have that $n=\mu(\mathcal{F}^*)/w_5=\mu(\mathcal{F}^*)/5$. So the running time for this part will be  $$O^*(1.3279^{\mu(\mathcal{F}^*)/w_5})=O^*(1.0584^{\mu(\mathcal{F}^*)}).$$

\subsection{Step 9}\label{subsec-step9}
In this step, we branch on a $(1,3)$-literal $x$. The two sub-branches are: $S_1=\{x\}$; $S_2=\{\overline{x}\}$. We have the following result:
\begin{lemma}
    The branching vector generated by step 9 is covered by
    \begin{equation}\label{vec-step9}
        [w_4+2w_3, w_4+6\delta_4]~\text{or}~[w_4+6\delta_4, w_4+2w_3].
    \end{equation}
\end{lemma}
\begin{proof}

By Lemma \ref{dec-1ltr}, we get that $\Delta_{S_1}\geq w_d+2w_3+\sum_{3\leq i\leq d}{n'_i(\overline{x})w_i}\geq w_4+2w_3$. By Lemma \ref{coro-assign2}, we have that $\Delta_{S_2}\geq \xi_{S_2}^{(1)} \geq w_d + j\delta_d\geq w_4+3\delta_4\geq \Delta_{S_1}$ since $\overline{x}$ is a $(3, 1)$-literal.

By Lemma \ref{dec-1ltr-sum}, we get that $\Delta_{S_1}+\Delta_{S_2}\geq 2w_d+2w_3+2(d-1)\delta_d= 2w_4+2w_3+6\delta_4$.

Since $\min(\Delta_{S_1}, \Delta_{S_2})\geq w_4+2w_3$ and $\Delta_{S_1}+\Delta_{S_2}\geq 2w_4+2w_3+6\delta_4$, we know that the branching vector of this case is covered by
$$
[w_4+2w_3, w_4+6\delta_4]~~\mbox{or}~~[w_4+6\delta_4, w_4+2w_3].
$$
\end{proof}
\subsection{Step 10}\label{subsec-step10}
In this step, we branch on a $(2,2)$-literal $x$. The two sub-branches are: $S_1=\{x\}$; $S_2=\{\overline{x}\}$. We have the following result:
\begin{lemma}
    The branching vector generated by step 10 is covered by
    \begin{equation}\label{vec-step10}
        [w_4+2\delta_4, w_4+6\delta_4]~\text{or}~[w_4+6\delta_4, w_4+2\delta_4].
    \end{equation}
\end{lemma}
\begin{proof}

By Lemma \ref{coro-assign2}, we get that $\Delta_{S_1}\geq \xi_{S_1}^{(1)} \geq w_d + j\delta_d=w_4+2\delta_4$ since $x$ is a $(2, 2)$-literal. Similarity, we can get that $\Delta_{S_2}\geq w_4+2\delta_4$.

By Lemma \ref{dec-sum}, we have
\begin{align*}
\Delta_{S_1}+\Delta_{S_2}
&\geq 2w_d + 2d\delta_d + (n'_3(x)+n'_3(\overline{x}))(2w_3-2\delta_d) \\
&~~~~+ \sum_{4\leq i\leq d}{(n'_i(x)+n'_i(\overline{x}))(w_i-2\delta_d)}\\
&= 2w_4 + 8\delta_4 + (n'_3(x)+n'_3(\overline{x}))(2w_3-2\delta_4)\\
&~~~~ + (n_4'(x)+n_4'(\overline{x}))(w_4-2\delta_4)\\
&= 2w_4+8\delta_4.
\end{align*}

Since $\min(\Delta_{S_1},\Delta_{S_2})\geq w_4+2\delta_4$ and $\Delta_{S_1}+\Delta_{S_2}\geq 2w_4+8\delta_4$, we know that the branching vector is covered by
$$
[w_4+2\delta_4, w_4+6\delta_4]~~\mbox{or}~~[w_4+6\delta_4, w_4+2\delta_4].
$$
\end{proof}

\subsection{Step 11}
All variables are $3$-variables now. We apply the $O^*(1.1279^n)$-time algorithm by Wahlstr{\"{o}}m~\cite{DBLP:conf/sat/Wahlstrom05} to solve this special case, where $n$ is the number of variables. For this case,
we have that $n=\mu(\mathcal{F})/w_3$. So the running time of this part is
 $$O^*((1.1279^{1/w_3})^{\mu(\mathcal{F})}).$$

\section{The Final Result}
Each one of the branching vectors above will generate a constraint in our quasiconvex program to solve the best value for $w_3$ and $w_4$.
Let $\alpha_i$ denote the  branching factor for branching vector ($i$) where $14\leq i\leq 21$.
We want to find the minimum value $\alpha$ such that $\alpha \leq \alpha_i$ and $\alpha \leq  1.1279^{1/w_3}$ (generated by Step 11)
under the assumptions  (\ref{weight1}) and (\ref{weight2}).
 By solving this quasiconvex program, we get that $\alpha=1.0646$ by letting $w_3=1.9234132344759123$ and $w_4=3.8468264689518246$.
 Note that $\alpha= 1.0646$ is greater than $1.0584$ the branching factor generated in Step 8. So 1.0646 is the worst branching factor in the whole algorithm. By (\ref{measure-leq-L}), we get the following result.
\begin{theorem}
    Algorithm \ref{main-algorithm} solves the SAT problem in $O^*(1.0646^L)$ time.
\end{theorem}


We also show the whole weight setting in Table \ref{tb-measure} and the branching vector of each step under the setting in Table \ref{tb-bv}.
\begin{table}
    \begin{center}
        \caption{The weight setting}\label{tb-measure}
        \begin{tabular}{l|l}
            \hline
            $w_1=w_2=0$ \\
            $w_3=1.9234132344759123$ ~~~&~~~ $\delta_3=1.9234132344759123$\\
            $w_4=3.8468264689518246$ ~~~&~~~ $\delta_4=1.9234132344759123$\\
            $w_5=5$ ~~~&~~~ $\delta_5=1.1531735310481754$\\
            $w_i=i(i\geq 6)$ ~~~&~~~ $\delta_i=1(i\geq 6)$ \\
            \hline
        \end{tabular}
    \end{center}
\end{table}

\begin{table}
\renewcommand\arraystretch{1.2}
\begin{center}
    \caption{The branching vector and factor for each step}\label{tb-bv}
    \begin{tabular}{l|c|c}
        \hline
        \textbf{Steps} & \textbf{Branching vectors} &\textbf{Branching factors}\\
        \hline
        Step 3 & $[w_6+\delta_6, w_6+11\delta_6]$ & $1.0636$\\
        \hline
        Step 4 & $[w_5+2w_3, w_5+8\delta_5]$ & $1.0632$\\
        \hline
        Step 5 & \makecell{$[w_5+3\delta_5, w_5+2w_3+5\delta_5]$\\$[w_5+2\delta_5, w_5+4w_3+4\delta_5]$} & $\makecell{1.0618\\1.0636}$\\
        \hline
        Step 6 & $[w_5+4\delta_5, w_5+7\delta_5]$ & $1.0636$\\
        \hline
        Step 7 & $[w_5+4\delta_5, w_5+5\delta_5+w_3]$ & $1.0646$\\
        \hline
        Step 8 & $O^*((1.3279^{1/w_5})^\mu)$ & $1.0584$ \\
        \hline
        Step 9 & $[w_4+2w_3, w_4+6\delta_4]$ & $1.0646$\\
        \hline
        Step 10 & $[w_4+2\delta_4, w_4+6\delta_4]$ & $1.0646$\\
        \hline
        Step 11 & $O^*((1.1279^{1/w_3})^\mu)$ & $1.0646$
        \\
        \hline
    \end{tabular}
\end{center}
\end{table}

From Table \ref{tb-bv}, we can see that we have four bottlenecks: Steps 7, 9, 10, and 11.
In fact, Steps 9, 10, and 11 have the same branching vector $[4w_3, 8w_3]$ under the assumption that $w_4=2w_3$ (for Step 11, the worst branching vector in~\cite{DBLP:conf/sat/Wahlstrom05} is $[4, 8]$).
The branching factor for these three steps will decrease if the value of $w_3$ increases. On the other hand, the branching factor for Step 7 will decrease if the value of $w_3$ decreases.
We set the best value of $w_3$ to balance them.
If we can either improve Step 7 or improve Steps 9, 10, and 11 together, then we may get a further improvement.  However, the improvement is very limited and several other bottlenecks will appear.


\section{Concluding Remarks}
In this paper, we show that the SAT problem can be solved in $O^*(1.0646^L)$ time, improving the previous bound in terms of the input length obtained more than 10 years ago.
Nowadays, improvement becomes harder and harder. However, SAT is one of the most important problems in exact and parameterized algorithms, and the state-of-the-art algorithms are frequently mentioned in the literature. Furthermore, in order to give a neat and clear analysis, we introduce a general analysis framework, which can even be used to simplify the analysis for other similar algorithms based on the measure-and-conquer method.
\nocite{*}
\bibliographystyle{splncs04}
