The Community for Technology Leaders
Green Image
Issue No. 07 - July (2015 vol. 64)
ISSN: 0018-9340
pp: 1830-1843
Chuan Luo , Key Laboratory of High Confidence Software Technologies of Ministry of Education, Peking University, Beijing, China
Shaowei Cai , State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
Wei Wu , Key Laboratory of High Confidence Software Technologies of Ministry of Education, Peking University, Beijing, China
Zhong Jie , Department of Online Game Business, NetEase, Inc., Hangzhou, Zhejiang, China
Kaile Su , Institute for Integrated and Intelligent Systems, Griffith University, Brisbane, QLD, Australia
ABSTRACT
The maximum satisfiability (MAX-SAT) problem, especially the weighted version, has extensive applications. Weighted MAX-SAT instances encoded from real-world applications may be very large, which calls for efficient approximate methods, mainlystochastic local search (SLS) ones. However, few works exist on SLS algorithms for weighted MAX-SAT. In this paper, we propose a new heuristic called CCM for weighted MAX-SAT. The CCM heuristic prefers to select a CCMP variable. By combining CCM withrandom walk, we design a simple SLS algorithm dubbed CCLS for weighted MAX-SAT. The CCLS algorithm is evaluated against a state-of-the-art SLS solver IRoTS and two state-of-the-art complete solvers namely akmaxsat_ls and New WPM2, on a broad range of weighted MAX-SAT instances. Experimental results illustrate that the quality of solution found by CCLS is much better than that found by IRoTS, akmaxsat_ls and New WPM2 on most industrial, crafted and random instances, indicating the efficiency and the robustness of the CCLS algorithm. Furthermore, CCLS is evaluated in the weighted and unweighted MAX-SAT tracks of incomplete solvers in the Eighth Max-SAT Evaluation (Max-SAT 2013), and wins four tracks in this evaluation, illustrating that the performance of CCLS exceeds the current state-of-the-art performance of SLS algorithms on solving MAX-SAT instances.
INDEX TERMS
Charge coupled devices, Algorithm design and analysis, Search problems, Complexity theory, Heuristic algorithms, Electronic mail, Robustness,make, Local search, weighted, maximum satisfiability, configuration checking
CITATION
Chuan Luo, Shaowei Cai, Wei Wu, Zhong Jie, Kaile Su, "CCLS: An Efficient Local Search Algorithm for Weighted Maximum Satisfiability", IEEE Transactions on Computers, vol. 64, no. , pp. 1830-1843, July 2015, doi:10.1109/TC.2014.2346196
394 ms
(Ver 3.3 (11022016))