New local search methods for partial MaxSAT
文献类型：期刊论文
| 作者 | Cai, Shaowei4; Luo, Chuan2,3; Lin, Jinkun2; Su, Kaile1 |
| 刊名 | ARTIFICIAL INTELLIGENCE
 |
| 出版日期 | 2016-11-01 |
| 卷号 | 240页码:1-18 |
| 关键词 | Partial MaxSAT Local search Hard and soft score Initialization |
| ISSN号 | 0004-3702 |
| DOI | 10.1016/j.artint.2016.07.006 |
| 英文摘要 | 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. |
| 资助项目 | China National 973 Program[2014CB340301] ; National Natural Science Foundation of China[61502464] ; National Natural Science Foundation of China[61370072] ; National Natural Science Foundation of China[61572234] ; Open Project Program of the State Key Laboratory of Mathematical Engineering and Advanced Computing[2016A06] ; ARC[DP150101618] |
| WOS研究方向 | Computer Science |
| 语种 | 英语 |
| WOS记录号 | WOS:000384851300001 |
| 出版者 | ELSEVIER SCIENCE BV |
| 源URL | [http://119.78.100.204/handle/2XEOYT63/8043]  |
| 专题 | 中国科学院计算技术研究所期刊论文_英文 |
| 通讯作者 | Cai, Shaowei |
| 作者单位 | 1.Griffith Univ, Inst Integrated & Intelligent Syst, Brisbane, Qld 4111, Australia 2.Peking Univ, Sch Elect Engn & Comp Sci, Beijing 100871, Peoples R China 3.Chinese Acad Sci, Inst Comp Technol, Beijing 100190, Peoples R China 4.Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing 100190, Peoples R China |
| 推荐引用方式 GB/T 7714 | Cai, Shaowei,Luo, Chuan,Lin, Jinkun,et al. New local search methods for partial MaxSAT[J]. ARTIFICIAL INTELLIGENCE,2016,240:1-18. |
| APA | Cai, Shaowei,Luo, Chuan,Lin, Jinkun,&Su, Kaile.(2016).New local search methods for partial MaxSAT.ARTIFICIAL INTELLIGENCE,240,1-18. |
| MLA | Cai, Shaowei,et al."New local search methods for partial MaxSAT".ARTIFICIAL INTELLIGENCE 240(2016):1-18. |
入库方式： OAI收割
来源：计算技术研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。