Resolution-based lower bounds in MaxSAT |
| |
Authors: | Chu Min Li Felip Manyà Nouredine Ould Mohamedou Jordi Planes |
| |
Affiliation: | 1.Hunan Normal University,Changsha,China;2.MIS,Université de Picardie Jules Verne,Amiens Cedex 01,France;3.Artificial Intelligence Research Institute (IIIA, CSIC),Bellaterra,Spain;4.Computer Science Department,Universitat de Lleida,Lleida,Spain |
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|