Therefore, how to branch more effectively in algorithms solving SAT
and MaxSAT has become critical. In particular, all existing parameterized
algorithms for MaxSAT and most known algorithms for SAT have
been focused on more effective branching strategies to further improve the
algorithm complexity. Define the degree of a variable \(x\)  in a CNF formula
\(F\)  to be the number of times \(x\)  and \(\bar{x}\)  appear in the formula. For
MaxSAT, it is well-known that branching on variables of large degree will
be sufficiently effective. On the other hand, variables of degree bounded by 2
can be handled efficiently based on the resolution principle [1]}. Recently,
Bliznets and Golovnev [2]} proposed new strategies for branching on
degree-3 variables more effectively and improved Chen and Kanj's algorithm
[3]}, which had stood as the best algorithm for MaxSAT
for 10 years.
