Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Breaking Cycle Structure to Improve Lower Bound for Max-SAT

Abstract : 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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées
Contributeur : Louise DESSAIVRE Connectez-vous pour contacter le contributeur
Soumis le : dimanche 10 avril 2022 - 11:39:27
Dernière modification le : samedi 6 août 2022 - 03:51:15




Yan-Li Liu, Chu-Min Li, Kun He, Yi Fan. Breaking Cycle Structure to Improve Lower Bound for Max-SAT. FRONTIERS IN ALGORITHMICS, FAW 2016, Jun 2016, Qingdao, China. pp.111-124, ⟨10.1007/978-3-319-39817-4\_12⟩. ⟨hal-03636432⟩



Consultations de la notice