Local search for Boolean satisfiability with configuration checking and subscore. (English) Zbl 1334.68200
Summary: This paper presents and analyzes two new efficient local search strategies for the Boolean Satisfiability (SAT) problem. We start by proposing a local search strategy called configuration checking (CC) for SAT. The CC strategy results in a simple local search algorithm for SAT called Swcc, which shows promising experimental results on random 3-SAT instances, and outperforms TNM, the winner of SAT Competition 2009.
However, the CC strategy for SAT is still in a nascent stage, and Swcc cannot yet compete with Sparrow2011, which won SAT Competition 2011 just after Swcc had been designed. The CC strategy seems too strict in that it forbids flipping those variables even with great scores, if they do not satisfy the CC criterion. We improve the CC strategy by adopting an aspiration mechanism, and get a new variable selection heuristic called configuration checking with aspiration (CCA). The CCA heuristic leads to an improved algorithm called Swcca, which exhibits state-of-the-art performance on random 3-SAT instances and crafted ones.
The third contribution concerns improving local search algorithms for random \( k\)-SAT instances with \(k>3\). Although the SAT community has made great achievements in solving random 3-SAT instances, the progress lags far behind on random \(k\)-SAT instances with \(k>3\). This work proposes a new variable property called subscore, which is utilized to break ties in the CCA heuristic when candidate variables for flipping have the same score. The resulting algorithm CCAsubscore is very efficient for solving random \( k\)-SAT instances with \(k>3\), and significantly outperforms other state-of-the-art ones. Combining Swcca and CCAsubscore, we obtain a local search SAT solver called CCASat, which was ranked first in the random track of SAT Challenge 2012.
Additionally, we perform theoretical analyses on the CC strategy and the subscore property, and show interesting results on these two heuristics. Particularly, our analysis indicates that the CC strategy is more effective for \( k\)-SAT with smaller \( k\), while the subscore notion is not suitable for solving random 3-SAT.
However, the CC strategy for SAT is still in a nascent stage, and Swcc cannot yet compete with Sparrow2011, which won SAT Competition 2011 just after Swcc had been designed. The CC strategy seems too strict in that it forbids flipping those variables even with great scores, if they do not satisfy the CC criterion. We improve the CC strategy by adopting an aspiration mechanism, and get a new variable selection heuristic called configuration checking with aspiration (CCA). The CCA heuristic leads to an improved algorithm called Swcca, which exhibits state-of-the-art performance on random 3-SAT instances and crafted ones.
The third contribution concerns improving local search algorithms for random \( k\)-SAT instances with \(k>3\). Although the SAT community has made great achievements in solving random 3-SAT instances, the progress lags far behind on random \(k\)-SAT instances with \(k>3\). This work proposes a new variable property called subscore, which is utilized to break ties in the CCA heuristic when candidate variables for flipping have the same score. The resulting algorithm CCAsubscore is very efficient for solving random \( k\)-SAT instances with \(k>3\), and significantly outperforms other state-of-the-art ones. Combining Swcca and CCAsubscore, we obtain a local search SAT solver called CCASat, which was ranked first in the random track of SAT Challenge 2012.
Additionally, we perform theoretical analyses on the CC strategy and the subscore property, and show interesting results on these two heuristics. Particularly, our analysis indicates that the CC strategy is more effective for \( k\)-SAT with smaller \( k\), while the subscore notion is not suitable for solving random 3-SAT.
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
References:
| [1] | Achlioptas, Dimitris, Random satisfiability, (Handbook of Satisfiability (2009), IOS Press), 245-270 |
| [2] | Audemard, Gilles; Simon, Laurent, Predicting learnt clauses quality in modern SAT solvers, (Proc. of IJCAI-09 (2009)), 399-404 |
| [3] | Balint, Adrian; Fröhlich, Andreas, Improving stochastic local search for SAT with a new probability distribution, (Proc. of SAT-10 (2010)), 10-15 · Zbl 1306.68150 |
| [4] | Balint, Adrian; Gall, Daniel; Kapler, Gregor; Retz, Robert, Experiment design and administration for computer clusters for SAT-solvers (edacc), JSAT, 7, 2-3, 77-82 (2010) |
| [5] | Balint, Adrian; Schöning, Uwe, Choosing probability distributions for stochastic local search and the role of make versus break, (Proc. of SAT-12 (2012)), 16-29 · Zbl 1273.68333 |
| [6] | Battiti, Roberto; Protasi, Marco, Reactive local search for the maximum clique problem, Algorithmica, 29, 4, 610-637 (2001) · Zbl 0985.68016 |
| [7] | Braunstein, Alfredo; Mézard, Marc; Zecchina, Riccardo, Survey propagation: An algorithm for satisfiability, Random Struct. Algorithms, 27, 2, 201-226 (2005) · Zbl 1087.68126 |
| [8] | Cai, Shaowei; Su, Kaile, Local search with configuration checking for SAT, (Proc. of ICTAI-11 (2011)), 59-66 · Zbl 1225.68242 |
| [9] | Cai, Shaowei; Su, Kaile, Configuration checking with aspiration in local search for SAT, (Proc. of AAAI-12 (2012)), 434-440 |
| [10] | Cai, Shaowei; Su, Kaile; Chen, Qingliang, EWLS: A new local search for minimum vertex cover, (Proc. of AAAI-10 (2010)), 45-50 |
| [11] | Cai, Shaowei; Su, Kaile; Luo, Chuan; Sattar, Abdul, NuMVC: An efficient local search algorithm for minimum vertex cover, J. Artif. Intell. Res., 46, 687-716 (2013) · Zbl 1280.90098 |
| [12] | Cai, Shaowei; Su, Kaile; Sattar, Abdul, Local search with edge weighting and configuration checking heuristics for minimum vertex cover, Artif. Intell., 175, 9-10, 1672-1696 (2011) · Zbl 1225.68242 |
| [13] | Eén, Niklas; Biere, Armin, Effective preprocessing in SAT through variable and clause elimination, (Proc. of SAT-05 (2005)), 61-75 · Zbl 1128.68463 |
| [14] | Gableske, Oliver, BossLS preprocessing and stochastic local search, (Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions (2012)), 10-11 |
| [15] | Gableske, Oliver; Heule, Marijn, EagleUP: Solving random 3-SAT using SLS with unit propagation, (Proc. of SAT-11 (2011)), 367-368 |
| [16] | Di Gaspero, Luca; Schaerf, Andrea, A composite-neighborhood tabu search approach to the traveling tournament problem, J. Heuristics, 13, 2, 189-207 (2007) |
| [17] | Gent, Ian P.; Walsh, Toby, Towards an understanding of hill-climbing procedures for SAT, (Proc. of AAAI-93 (1993)), 28-33 |
| [18] | Glover, Fred, Tabu search - part i, ORSA J. Comput., 1, 3, 190-206 (1989) · Zbl 0753.90054 |
| [19] | Glover, Fred, Tabu search - part ii, ORSA J. Comput., 2, 1, 4-32 (1990) · Zbl 0771.90084 |
| [20] | Hoos, Holger H.; Stützle, Thomas, Local search algorithms for SAT: An empirical evaluation, J. Autom. Reason., 24, 4, 421-481 (2000) · Zbl 0961.68039 |
| [21] | Hoos, Holger H.; Stützle, Thomas, Stochastic Local Search: Foundations & Applications (2005), Elsevier/Morgan Kaufmann · Zbl 1126.68032 |
| [22] | Hutter, Frank; Tompkins, Dave A. D.; Hoos, Holger H., Scaling and probabilistic smoothing: Efficient dynamic local search for SAT, (Proc. of CP-02 (2002)), 233-248 |
| [23] | Kautz, Henry A.; Sabharwal, Ashish; Selman, Bart, Incomplete algorithms, (Handbook of Satisfiability (2009), IOS Press), 185-203 |
| [24] | Kirkpatrick, Scott; Selman, Bart, Critical behavior in the satisfiability of random boolean formulae, Science, 264, 1297-1301 (1994) · Zbl 1226.68097 |
| [25] | Kroc, Lukas; Sabharwal, Ashish; Selman, Bart, An empirical study of optimal noise and runtime distributions in local search, (Proc. of SAT-10 (2010)), 346-351 · Zbl 1306.68163 |
| [26] | Li, Chu Min; Huang, Wen Qi, Diversification and determinism in local search for satisfiability, (Proc. of SAT-05 (2005)), 158-172 · Zbl 1128.68472 |
| [27] | Li, Chu Min; Li, Yu, Satisfying versus falsifying in local search for satisfiability - (poster presentation), (Proc. of SAT-12 (2012)), 477-478 |
| [28] | Li, Chu Min; Wei, Wanxia; Li, Yu, Exploiting historical relationships of clauses and variables in local search for satisfiability - (poster presentation), (Proc. of SAT-12 (2012)), 479-480 |
| [29] | Li, Chu Min; Li, Yu, Description of sattime2012, (Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions (2012)), 53 |
| [30] | Luo, Chuan; Cai, Shaowei; Wu, Wei; Su, Kaile, Focused random walk with configuration checking and break minimum for satisfiability, (Proc. of CP-13 (2013)), 481-496 |
| [31] | Luo, Chuan; Su, Kaile; Cai, Shaowei, Improving local search for random 3-SAT using quantitative configuration checking, (Proc. of ECAI-12 (2012)), 570-575 · Zbl 1327.68225 |
| [32] | Mazure, Bertrand; Sais, Lakhdar; Grégoire, Éric, Tabu search for SAT, (Proc. of AAAI-97 (1997)), 281-285 |
| [33] | Mertens, Stephan; Mézard, Marc; Zecchina, Riccardo, Threshold values of random \(k\)-SAT from the cavity method, Random Struct. Algorithms, 28, 3, 340-373 (2006) · Zbl 1094.68035 |
| [34] | McAllester, David A.; Selman, Bart; Kautz, Henry A., Evidence for invariants in local search, (Proc. of AAAI-97 (1997)), 321-326 |
| [35] | Mézard, Marc, Passing messages between disciplines, Science, 301, 1685-1686 (2003) |
| [36] | Michiels, Wil; Aarts, Emile H. L.; Korst, Jan H. M., Theoretical Aspects of Local Search (2007), Springer · Zbl 1130.90061 |
| [37] | Papadimitriou, Christos H., On selecting a satisfying truth assignment, (Proc. of FOCS-91 (1991)), 163-169 |
| [38] | Paturi, Ramamohan; Pudlák, Pavel; Saks, Michael E.; Zane, Francis, An improved exponential-time algorithm for \(k\)-SAT, J. ACM, 52, 3, 337-364 (2005) · Zbl 1297.68217 |
| [39] | Nghia Pham, Duc; Duong, Thach-Thao; Sattar, Abdul, Trap avoidance in local search using pseudo-conflict learning, (Proc. of AAAI-12 (2012)), 542-548 |
| [40] | Roussel, Olivier, Description of ppfolio 2012, (Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions (2012)), 46 |
| [41] | Salhi, Said, Defining tabu list size and aspiration criterion within tabu search methods, Computers Oper. Res., 29, 1, 67-86 (2002) · Zbl 1020.90027 |
| [42] | Seitz, Sakari; Alava, Mikko; Orponen, Pekka, Focused local search for random 3-satisfiability, J. Stat. Mech., P06006 (2005) · Zbl 1128.68482 |
| [43] | Selman, Bart; Kautz, Henry A.; Cohen, Bram, Noise strategies for improving local search, (Proc. of AAAI-94 (1994)), 337-343 |
| [44] | Smyth, Kevin; Hoos, Holger H.; Stützle, Thomas, Iterated robust tabu search for MAX-SAT, (Proc. of Canadian Conference on AI (2003)), 129-144 |
| [45] | Stelzmann, Robert, The stochastic local search solver: ssa, (Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions (2012)), 63 |
| [46] | Thornton, John; Nghia Pham, Duc; Bain, Stuart; Ferreira, Valnir, Additive versus multiplicative clause weighting for SAT, (Proc. of AAAI-04 (2004)), 191-196 |
| [47] | Tompkins, Dave A. D.; Balint, Adrian; Hoos, Holger H., Captain jack: New variable selection heuristics in local search for SAT, (Proc. of SAT-11 (2011)), 302-316 · Zbl 1330.68277 |
| [48] | Tompkins, Dave A. D.; Hoos, Holger H., Dynamic scoring functions with variable expressions: New SLS methods for solving SAT, (Proc. of SAT-10 (2010)), 278-292 · Zbl 1306.68176 |
| [49] | Wotzlaw, Andreas; van der Grinten, Alexander; Speckenmeyer, Ewald; Porschen, Stefan, pfolioUZK: Solver description, (Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions (2012)), 45 |
| [50] | Xu, Lin; Hutter, Frank; Shen, Jonathan; Hoos, Holger H.; Leyton-Brown, Kevin, Satzilla2012: Improved algorithm selection based on cost-sensitive classification models, (Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions (2012)), 57 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
