Name
Abstract | ||
|---|---|---|
We investigate the role of cycles structures (i.e., subsets of clauses of the form $\bar{l}_{1}\vee l_{2}, \bar{l}_{1}\vee l_{3},\bar{l}_{2}\vee\bar{l}_{3}$) 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 $\bar{l}_{1},l_{1}\vee\bar{l}_{2}\vee\bar{l}_{3},\bar{l}_{1}\vee l_{2}\vee l_{3}$ 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 MaxSatz c . Our experiments on weighted MaxSAT and Partial MaxSAT instances indicate that MaxSatz c substantially improves MaxSatz on many hard random, crafted and industrial instances. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-02777-2_43 | SAT |
Keywords | Field | DocType |
cycles structure,modern maxsat solvers,cycle structure,underestimation component,weighted maxsat,maxsat resolution,exploiting cycle structures,partial maxsat instance,inconsistent subformulas,vee l,failed literal detection,time change,lower bound | Maximum satisfiability problem,Discrete mathematics,Combinatorics,Upper and lower bounds,Unit propagation,Solver,Mathematics | Conference |
Volume | ISSN | Citations |
5584 | 0302-9743 | 22 |
PageRank | References | Authors |
1.07 | 13 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chu Min Li | 1 | 1194 | 85.65 |
| Felip Manyà | 2 | 787 | 59.52 |
| Nouredine Mohamedou | 3 | 22 | 1.07 |
| Jordi Planes | 4 | 486 | 31.38 |