Dealing with 4-variables by resolution: An improved MaxSAT algorithm

We study techniques for solving the Maximum Satisfiability problem (MaxSAT). Our focus is on variables of degree 4. We identify cases for degree-4 variables and show how the resolution principle and the kernelization techniques can be nicely integrated to achieve more efficient algorithms for the MaxSAT problem. As a result, we present an algorithm of time O⁎(1.3248k) for the MaxSAT problem, improving the previous best upper bound O⁎(1.358k) by Ivan Bliznets and Alexander Golovnev.