Resolution-based lower bounds in MaxSAT
Resolution-based lower bounds in MaxSAT
复制标题
DOI：
10.1007/s10601-010-9097-9
复制
发表时间：
2010-10
期刊：
影响因子：
1.6
通讯作者：
Chu Min Li;F. Manyà;N. Mohamedou;Jordi Planes
中科院分区：
文献类型：
--
作者：
Chu Min Li;F. Manyà;N. Mohamedou;Jordi Planes
在分支和有界MaxSAT求解器中实现的下界（LB）是获得竞争求解器的决定性因素。在MaxSatz和MiniMaxSat等现代求解器中，LB依赖于低估和推理组件的合作。实际上，一些解算器的低估分量指导了在达到冲突和发现某些结构时推理分量的应用。在本文中，我们分析了在MaxSatz发展过程中实现的低估组件的算法和逻辑方面。从算法的角度来看，我们定义了在up中选择单元子句的新策略（在up中LB的低估是使用单元传播检测到的独立不一致子公式的数量），扩展了具有失败文字检测的fup，以及在存在循环结构的情况下应用具有失败文字检测的upaugmented时指导MaxSAT分辨率应用的巧妙启发式。从逻辑的角度来看，我们证明ups检测到的不一致子公式是最低限度的不可满足的，但是如果添加了失败的文字检测，则此属性不成立。在upaugmented检测到的冲突中存在循环结构的情况下，我们证明了MaxSAT分辨率的应用产生了更小的不一致子公式，此外，还产生了可用于改进LB的附加子句。进行的实证调查表明，本文中描述的LB技术导致了更高质量的LB。
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 inUP(the underestimation of LB inUPis the number of independent inconsistent subformulas detected using unit propagation), the extension ofUPwith failed literal detection, and a clever heuristic for guiding the application of MaxSAT resolution whenUPaugmented 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 byUPare minimally unsatisfiable, but this property does not hold if failed literal detection is added. In the presence of cycle structures in conflicts detected byUPaugmented 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.