Name
Abstract | ||
|---|---|---|
The lower bound (LB) implemented in branch and bound MaxSAT solvers is decisive for obtaining a competitive solver. In modern solvers like MaxSatz and MiniMaxSat, the LB relies on the cooperation of the underestimation and inference components. Actually, the underestimation component of some solvers guides the application of the inference component when a conflict is reached and certain structures are found. In this paper we analyze algorithmic and logical aspects of the underestimation components that have been implemented in MaxSatz during its evolution. From an algorithmic point of view, we define novel strategies for selecting unit clauses in UP (the underestimation of LB in UP is the number of independent inconsistent subformulas detected using unit propagation), the extension of UP with failed literal detection, and a clever heuristic for guiding the application of MaxSAT resolution when UP augmented with failed literal detection is applied in the presence of cycles structures. From a logical point of view, we prove that the inconsistent subformulas detected by UP are minimally unsatisfiable, but this property does not hold if failed literal detection is added. In the presence of cycle structures in conflicts detected by UP augmented with failed literal detection, we prove that the application of MaxSAT resolution produces smaller inconsistent subformulas and, besides, generates additional clauses that may be used to improve the LB. The conducted empirical investigation indicates that the LB techniques described in this paper lead to better quality LBs. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/s10601-010-9097-9 | Constraints |
Keywords | Field | DocType |
MaxSAT,Lower bound,Inference,Underestimation | Maximum satisfiability problem,Heuristic,Branch and bound,Mathematical optimization,Upper and lower bounds,Inference,Algorithm,Unit propagation,Solver,Mathematics | Journal |
Volume | Issue | ISSN |
15 | 4 | 1383-7133 |
Citations | PageRank | References |
20 | 0.99 | 17 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chu Min Li | 1 | 1194 | 85.65 |
| Felip Manyà | 2 | 787 | 59.52 |
| Nouredine Ould Mohamedou | 3 | 24 | 1.48 |
| Jordi Planes | 4 | 486 | 31.38 |