Dealing With 4-Variables by Resolution: An Improved MaxSAT Algorithm

TL;DR

This paper introduces an improved MaxSAT algorithm that efficiently handles degree-4 variables by integrating resolution and kernelization techniques, achieving a better exponential time bound than previous methods.

Contribution

It presents a novel algorithm for MaxSAT that specifically targets degree-4 variables, combining resolution and kernelization to enhance efficiency.

Findings

Achieved a time complexity of O*(1.3248^k) for MaxSAT.

Improved the previous upper bound of O*(1.358^k).

Demonstrated effective integration of resolution and kernelization techniques.

Abstract

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.3248^k)$ for the MaxSAT problem, improving the previous best upper bound $O^*(1.358^k)$ by Ivan Bliznets and Alexander.