Breaking Cycle Structure to Improve Lower Bound for Max-SAT
Résumé
Many practical optimization problems can be translated to Max-SAT and solved using a Branch-and-Bound (BnB) Max-SAT solver. The performance of a BnB Max-SAT solver heavily depends on the quality of the lower bound. Lower bounds in state-of-the-art BnB Max-SAT solvers are based on detecting inconsistent subsets of clauses and then on applying Max-SAT resolution to transform each inconsistent subset of clauses into an equivalent set containing an empty clause and a number of compensation clauses. In this paper, we focus on the transformation of the inconsistent subsets of clauses containing one unit clause and a number of binary clauses. We show that Max-SAT resolution generates a lot of ternary compensation clauses when transforming such an inconsistent set, deteriorating the quality of the lower bound, and propose a new inference rule, called cycle breaking rule, to transform the inconsistent set. We prove the correctness of the rule and implement it in a new BnB Max-SAT solver called Brmaxsat. Experimental results showed that cycle breaking rule is very effective, especially on Max-2SAT.