Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front. Comput. Sci.    2019, Vol. 13 Issue (1) : 86-98    https://doi.org/10.1007/s11704-018-7107-z
RESEARCH ARTICLE
Empirical investigation of stochastic local search for maximum satisfiability
Yi CHU1,2, Chuan LUO1,3, Shaowei CAI4, Haihang YOU1()
1. State Key Laboratory of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100190, China
2. University of Chinese Academy of Sciences, Beijing 100049, China
3. State Key Laboratory of Mathematical Engineering and Advanced Computing,Wuxi 214125, China
4. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
 Download: PDF(612 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
Abstract

The maximum satisfiability (MAX-SAT) problem is an important NP-hard problem in theory, and has a broad range of applications in practice. Stochastic local search (SLS) is becoming an increasingly popular method for solving MAX-SAT. Recently, a powerful SLS algorithm called CCLS shows efficiency on solving random and crafted MAX-SAT instances. However, the performance of CCLS on solving industrial MAX-SAT instances lags far behind. In this paper, we focus on experimentally analyzing the performance of SLS algorithms for solving industrial MAXSAT instances. First, we conduct experiments to analyze why CCLS performs poor on industrial instances. Then we propose a new strategy called additive BMS (Best from Multiple Selections) to ease the serious issue. By integrating CCLS and additive BMS, we develop a new SLS algorithm for MAXSAT called CCABMS, and related experiments indicate the efficiency of CCABMS. Also, we experimentally analyze the effectiveness of initialization methods on SLS algorithms for MAX-SAT, and combine an effective initialization method with CCABMS, resulting in an enhanced algorithm. Experimental results show that our enhanced algorithm performs better than its state-of-the-art SLS competitors on a large number of industrial MAX-SAT instances.

Keywords empirical investigation      stochastic local search      maximum satisfiability      industrial instances      additive BMS     
Corresponding Author(s): Haihang YOU   
Just Accepted Date: 24 November 2017   Online First Date: 04 September 2018    Issue Date: 31 January 2019
 Cite this article:   
Yi CHU,Chuan LUO,Shaowei CAI, et al. Empirical investigation of stochastic local search for maximum satisfiability[J]. Front. Comput. Sci., 2019, 13(1): 86-98.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-018-7107-z
https://academic.hep.com.cn/fcs/EN/Y2019/V13/I1/86
1 S DPrestwich. CNF encodings. Handbook of Satisfiability. 2009, 75–97
2 C MLi, F Manyà. MaxSAT, hard and soft constraints. Handbook of Satisfiability, 2009, 185: 613–631
3 KSmyth, H HHoos, TStützle. Iterated robust tabu search for MAXSAT. In: Proceedings of Conference of the Canadian Society for Computational Studies of Intelligence. 2003, 129–144
4 QYang, KWu, YJiang. Learning action models from plan examples using weighted MAX-SAT. Artificial Intelligence, 2007, 171(2-3): 107–143
https://doi.org/10.1016/j.artint.2006.11.005
5 YChen, S Safarpour, JMarques-Silva, A GVeneris. Automated design debugging with maximum satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2010, 29(11): 1804–1817
https://doi.org/10.1109/TCAD.2010.2061270
6 EDemirovic, NMusliu. MaxSAT-based large neighborhood search for high school timetabling. Computers & Operations Research, 2017, 78: 172–180
https://doi.org/10.1016/j.cor.2016.08.004
7 WHuang, D A Kitchaev, SDacek, Z QRong, AUrban, SCao, C Luo, GCeder. Finding and proving the exact ground state of a generalized Ising model by convex optimization and MAX-SAT. Physical Review B, 2016, 94(13): 134424
https://doi.org/10.1103/PhysRevB.94.134424
8 JBerg, M Järvisalo, BMalone. Learning optimal bounded treewidth bayesian networks via maximum satisfiability. Artifical Intelligence and Statistics. 2014, 86–95
9 H LChieu, W SLee. Relaxed survey propagation for the weighted maximum satisfiability problem. Journal of Artificial Intelligence Research, 2009, 36: 229–266
https://doi.org/10.1613/jair.2808
10 CLuo, SCai, KSu, WHuang. CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. Artificial Intelligence, 2017, 243: 26–44
https://doi.org/10.1016/j.artint.2016.11.001
11 HLin, KSu. Exploiting inference rules to compute lower bounds for MAX-SAT solving. In: Proceedings of IJCAI. 2007, 2334–2339
12 HLin, KSu, C MLi. Within-problem learning for efficient lower bound computation in Max-SAT solving. In: Proceedings of AAAI. 2008, 351–356
13 C MLi, F Manyà, N OMohamedou, JPlanes , Exploiting cycle structures inMax-SAT. In: Proceedings of International Conference on Theory and Applications of Satisfiability Testing. 2009, 467–480
14 CAnsótegui, M L Bonet, JLevy. SAT-based MaxSAT algorithms. Artificial Intelligence, 2013, 196: 77–105
https://doi.org/10.1016/j.artint.2013.01.002
15 CAnsótegui, M L Bonet, JGabàs, JLevy. Improving WPM2 for (weighted) partial MaxSAT. In: Proceedings of International Conference on Principles and Practice of Constraint Programming. 2013, 117–132
https://doi.org/10.1007/978-3-642-40627-0_12
16 NNarodytska, F Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In: Proceedings of AAAI. 2014, 2717–2723
17 H HHoos, T Stützle. Stochastic Local Search: Foundations & Applications. San Francisoc: Morgan Kaufmann, 2004
18 SCai, CLuo, JThornton, K Su. Tailoring local search for partial MaxSAT. In: Proceedings of AAAI. 2014, 2623–2629
19 SCai, KSu, CLuo, A Sattar. NuMVC: an efficient local search algorithm for minimum vertex cover. Journal of Artificial Intelligence Research, 2013, 46: 687–716
https://doi.org/10.1613/jair.3907
20 SCai. Balance between complexity and quality: local search for minimum vertex cover in massive graphs. In: Proceedings of IJCAI. 2015, 747–753
21 ZZhang, HHe, ZLuo, H Qin, SGuo. An efficient forest-based tabu search algorithm for the split-delivery vehicle routing problem. In: Proceedings of AAAI. 2015, 3432–3438
22 SUmetani. Exploiting variable associations to configure efficient local search in large-scale set partitioning problems. In: Proceedings of AAAI. 2015, 1226–1232
23 JLin, CLuo, SCai, K Su, DHao, LZhang. TCA: an efficient twomode meta-heuristic algorithm for combinatorial test generation. In: Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2015, 494–505
https://doi.org/10.1109/ASE.2015.61
24 WGuo, GLiu, GChen, S Peng. A hybrid multi-objective pso algorithm with local search strategy for vlsi partitioning. Frontiers of Computer Science, 2014, 8(2): 203–216
https://doi.org/10.1007/s11704-014-3008-y
25 BSelman, H J Levesque, D GMitchell. A new method for solving hard satisfiability problems. In: Proceedings of AAAI. 1992, 440–446
26 BSelman, H AKautz, BCohen. Noise strategies for improving local search. In: Proceedings of AAAI. 1994, 337–343
27 YJiang, HKautz, BSelman. Solving problems with hard and soft constraints using a stochastic algorithm for MAX-SAT. In: Proceedings of the 1st International Joint Workshop on Artificial Intelligence and Operations Research. 1995, 20
28 B WWah, YShang. Discrete lagrangian-based search for solving MAX-SAT problems. In: Proceedings of IJCAI. 1997, 378–383
29 PMills, E P KTsang. Guided local search for solving SAT and weighted MAX-SAT problems. Journal of Automated Reasoning, 2000, 24(1/2): 205–223
https://doi.org/10.1023/A:1006343127545
30 MYagiura, T Ibaraki. Efficient 2 and 3-flip neighborhood search algorithms for the MAX SAT: experimental evaluation. Journal of Heuristics, 2001, 7(5): 423–442
https://doi.org/10.1023/A:1011306011437
31 K LSadowski, P A NBosman, DThierens. On the usefulness of linkage processing for solving MAX-SAT. In: Proceedings of GECCO. 2013, 853–860
https://doi.org/10.1145/2463372.2463474
32 DHains, D Whitley, A EHowe, WChen. Hyperplane initialized local search for MAXSAT. In: Proceedings of the 15th Annual Conference on Genetic and Evolutionary Computation. 2013, 805–812
https://doi.org/10.1145/2463372.2463468
33 DWhitley, A EHowe, DHains. Greedy or not? best improving versus first improving stochastic local search for MAXSAT. In: Proceedings of AAAI. 2013, 940–946
34 LKroc, A Sabharwal, C PGomes, BSelman. Integrating systematic and local search paradigms: a new strategy for MaxSAT. In: Proceedings of IJCAI. 2009, 544–551
35 SCai, KSu. Local search for Boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 2013, 204: 75–98
https://doi.org/10.1016/j.artint.2013.09.001
36 CLuo, SCai, WWu, ZJie, KSu. CCLS: an efficient local search algorithm for weighted maximum satisfiability. IEEE Transactions on Computers, 2015, 64(7): 1830–1843
https://doi.org/10.1109/TC.2014.2346196
37 JGoffinet, R Ramanujan. Monte-carlo tree search for the maximum satisfiability problem. In: Proceedings of International Conference on Prmciples and Practice of Constraint Programming. 2016, 251–267
https://doi.org/10.1007/978-3-319-44953-1_17
38 MWagner. MaxSAT solver SC2016. Max-SAT Evaluation, 2016
39 YFan, ZMa, KSu, ASattar, CLi. Ramp: a local search solver based on make-positive variables. Max-SAT Evaluation, 2016
40 SCai, CLuo, JLin, K Su. New local search methods for partial maxsat. Artificial Intelligence, 2016, 240: 1–18
https://doi.org/10.1016/j.artint.2016.07.006
41 ORoussel. Controlling a solver execution with the runsolver tool. Journal on Satisfiability, Boolean Modeling and Computation, 2011, 7(4): 139–144
42 SCai, JLin. Fast solving maximum weight clique problem in massive graphs. In: Proceedings of IJCAI. 2016, 568–574
43 YWang, SCai, MYin. Two efficient local search algorithms for maximum weight clique problem. In: Proceedings of AAAI. 2016, 805–811
44 FHutter, H HHoos, KLeyton-Brown, TStützle. ParamILS: an automatic algorithm configuration framework. Journal of Artificial Intelligence Research, 2009, 36: 267–306
https://doi.org/10.1613/jair.2861
45 FHutter, H HHoos, KLeyton-Brown. Sequential model-based optimization for general algorithm configuration. In: Proceedings of International Conference on Learning and Intelligent Optimization. 2011, 507–523
https://doi.org/10.1007/978-3-642-25566-3_40
46 H HHoos. An adaptive noise mechanism for WalkSAT. In: Proceedings of AAAI. 2002, 655–660
47 JThornton, D NPham, SBain, VFerreira Jr. Additive versus multiplicative clause weighting for SAT. In: Proceedings of AAAI. 2004, 191–196
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed