New local search methods for partial MaxSAT
New local search methods for partial MaxSAT
复制标题
部分 MaxSAT 的新本地搜索方法
DOI：
10.1016/j.artint.2016.07.006
复制
发表时间：
2016-11-01
影响因子：
14.4
通讯作者：
Su, Kaile
中科院分区：
文献类型：
--
作者：
Cai, Shaowei;Luo, Chuan;Su, Kaile
最大可满足性(MaxSAT)是可满足性(SAT)问题的优化版本。部分最大可满足性(PMS)是MaxSAT的推广，它涉及硬子句和软子句，具有重要的现实应用。局部搜索是解决SAT和MaxSAT问题的一种流行方法，并在这两个问题上取得了巨大的成功。然而，遗憾的是，PMS的本地搜索算法并没有从SAT和MaxSAT的本地搜索技术中获益太多，这主要是因为它同时包含硬子句和软子句。这一特点使得设计有效的PMS局部搜索算法变得更具挑战性，这可能是该方向十多年来停滞不前的原因。利用前三种思想，包括硬子句加权、软硬分值分离和基于软硬分值的变量选择启发式算法，提出了一种PMS局部搜索算法DIST。第四种思想是在硬单元子句上使用带优先级的单元传播来生成初始赋值，并将其用于改进工业实例上的DIST，从而得到了DistUP算法。通过对MaxSAT评估2014年的所有PMS基准的实验评估，验证了我们的求解器和想法的有效性。根据我们的实验结果，DIST在所有基准上都比以前的局部搜索解算器有显著的改进。我们还将我们的求解器与最先进的完全PMS求解器和最先进的投资组合求解器进行了比较，结果表明我们的求解器在随机和精心制作的实例中具有更好的性能，但在工业实例中性能较差。DIST的良好表现也得到了以下事实的印证：DIST在2014年MaxSAT评估的不完全解算器轨道上赢得了所有随机和精心制作的PMS和加权PMS类别。(C)2016爱思唯尔B.V.保留所有权利。
Maximum Satisfiability (MaxSAT) is the optimization version of the Satisfiability (SAT) problem. Partial Maximum Satisfiability (PMS) is a generalization of MaxSAT which involves hard and soft clauses and has important real world applications. Local search is a popular approach to solving SAT and MaxSAT and has witnessed great success in these two problems. However, unfortunately, local search algorithms for PMS do not benefit much from local search techniques for SAT and MaxSAT, mainly due to the fact that it contains both hard and soft clauses. This feature makes it more challenging to design efficient local search algorithms for PMS, which is likely the reason of the stagnation of this direction in more than one decade.In this paper, we propose a number of new ideas for local search for PMS, which mainly rely on the distinction between hard and soft clauses. The first three ideas, including weighting for hard clauses, separating hard and soft score, and a variable selection heuristic based on hard and soft score, are used to develop a local search algorithm for PMS called Dist. The fourth idea, which uses unit propagation with priority on hard unit clauses to generate the initial assignment, is used to improve Dist on industrial instances, leading to the DistUP algorithm.The effectiveness of our solvers and ideas is illustrated through experimental evaluations on all PMS benchmarks from the MaxSAT Evaluation 2014. According to our experimental results, Dist shows a significant improvement over previous local search solvers on all benchmarks. We also compare our solvers with state-of-the-art complete PMS solvers and a state-of-the-art portfolio solver, and the results show that our solvers have better performance in random and crafted instances but worse in industrial instances. The good performance of Dist has also been confirmed by the fact that Dist won all random and crafted categories of PMS and Weighted PMS in the incomplete solvers track of the MaxSAT Evaluation 2014. (C) 2016 Elsevier B.V. All rights reserved.