Breaking Cycle Structure to Improve Lower Bound for Max-SAT - Archive ouverte HAL Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

Breaking Cycle Structure to Improve Lower Bound for Max-SAT

, (1, 2) , (3) ,
1
2
3

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.
Fichier non déposé

Dates et versions

hal-03636432 , version 1 (10-04-2022)

Identifiants

Citer

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⟩
26 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook Twitter LinkedIn More