Improved Max-SAT Complete Algorithm Based Slacking Inconsistent Set

Maximum satisfiability problem(Max-SAT) is an important generalization of a classic NP-hard problem, Satisfiability problem(SAT), while Max-SAT is also a classic NP-complete problem. Max-SAT is very important in the field of computer science and theory in both theory and practice. Many industrial problems, for example circuit designing, scheduling system, can be transformed into a Max-SAT problem. The current state-of-the-art of exact Max-SAT solvers is based SAT and based branch and bounds. The key point of designing a competive Max-SAT complete algorithm based on branch and bounds is to improve the lower bounds and reduce the upper bounds. Over the past decades, the Max-SAT solvers have made great advances, some technology, like unit propagation, inferencr rules have made great progress.Improving the lower bounds is the key to improve the branch and bounds Max-SAT algorithm efficiently. Based on the Maxsatz2013 algorithm proposed in 2013, which used unit propagation and failed literals detecting, we add a new strategy named slacking inconsistent set, in the process of the underestimation of lower bounds, which named Smaxsatz. By inserting a slack variable to these clauses, and giving a constraint that only one slack variable can be assigned 1 for the inconsistent set, an inconsistent set has been eliminated, thus means slacking inconsistent set. Then add the new clauses set into the CNF, use unit propagation to find more disjoint inconsistent sets and hence improve the lower bounds.At last, the new algorithm and Maxsatz2013 algorithm were tested with the instances of the Max-SAT evaluation. Experimental results showed the feasibility and effectiveness of the algorithm with slacking inconsistent sets, as it reduced the computation obviously.