Exploiting Cycle Structures in Max-SAT

We investigate the role of cycles structures (i.e., subsets of clauses of the form ¯l1 ∨ l2, ¯l1 ∨ l3, ¯l2 ∨ ¯l3) in the quality of the lower bound (LB) of modern MaxSAT solvers. Given a cycle structure, we have two options: (i) use the cycle structure just to detect inconsistent subformulas in the underestimation component, and (ii) replace the cycle structure with ¯l1, l1 ∨¯l2 ∨¯l3, ¯l1 ∨ l2 ∨ l3 by applying MaxSAT resolution and, at the same time, change the behaviour of the underestimation component. We first show that it is better to apply MaxSAT resolution to cycle structures occurring in inconsistent subformulas detected using unit propagation or failed literal detection. We then propose a heuristic that guides the application of MaxSAT resolution to cycle structures during failed literal detection, and evaluate this heuristic by implementing it in MaxSatz, obtaining a new solver called MaxSatzc. Our experiments on weighted MaxSAT and Partial MaxSAT instan...

• Type: Conference
• Year: 2009
• Where: SAT
• Authors: Chu Min Li, Felip Manyà, Nouredine Ould Mohamedou, Jordi Planes
• Keywords: Cycle Structures, Hardware, Inconsistent Subformulas, MaxSAT Resolution, SAT 2009