Efficient application of Max-SAT resolution on inconsistent subsets

Abstract

Max-SAT resolution is the adaption of the powerful SAT resolution rule for the Max-SAT problem. One of the differences between these two rules is that Max-SAT resolution adds, besides the resolvent, several compensation clauses to keep the formula's equivalency. We address in this paper the problem of reducing both the number and the size of these compensation clauses. We show that the order in which the Max-SAT resolution steps are applied on the inconsistent subsets of clauses has a direct impact on the number and the sizes of the compensation clauses added to the formula. Based on this observation, we present a new algorithm for applying Max-SAT resolution on inconsistent subsets which reduces the number and the sizes of the produced compensation clauses. We demonstrate experimentally the interest of our contribution. © 2014 Springer International Publishing Switzerland.