A Refined Branching Algorithm for the Maximum Satisfiability Problem

The Maximum satisfiability problem ( MaxSAT ) is a fundamental NP-hard problem which has significant applications in many areas. Based on refined observations, we derive a branching algorithm of running time O^*(1.2989^m) for the MaxSAT problem, where m denotes the number of clauses in the given CNF formula. Our algorithm considerably improves the previous best result O^*(1.3248^m) published in 2004. For our purpose, we derive improved branching strategies for variables of degrees 3, 4, and 5. The worst case of our branching algorithm is at certain degree-4 variables. To serve the branching rules, we also propose a variety of reduction rules which can be exhaustively applied in polynomial time.