Abstract
This paper presents a stochastic local search (SLS) solver for SAT named CCAnr, which is based on the configuration checking strategy and has good performance on non-random SAT instances. CCAnr switches between two modes: it flips a variable according to the CCA (configuration checking with aspiration) heuristic if any; otherwise, it flips a variable in a random unsatisfied clause (which we refer to as the focused local search mode). The main novelty of CCAnr lies on the greedy heuristic in the focused local search mode, which contributes significantly to its good performance on structured instances. Previous two-mode SLS algorithms usually utilize diversifying heuristics such as age or randomized strategies to pick a variable from the unsatisfied clause. Our experiments on combinatorial and application benchmarks from SAT Competition 2014 show that CCAnr has better performance than other state-of-the-art SLS solvers on structured instances, and its performance can be further improved by using a preprocessor CP3. Our results suggest that a greedy heuristic in the focused local search mode might be helpful to improve SLS solvers for solving structured SAT instances.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Balint, A., Fröhlich, A.: Improving stochastic local search for sat with a new probability distribution. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 10–15. Springer, Heidelberg (2010)
Balint, A., Manthey, N.: SparrowToRiss. In: Proc. of SAT Competition 2014: Solver and Benchmark Descriptions, p. 77 (2014)
Cai, S., Luo, C., Su, K.: CCAnr+glucose in SAT competition 2014. In: Proc. of SAT Competition 2014: Solver and Benchmark Descriptions, p. 17 (2014)
Cai, S., Su, K.: Configuration checking with aspiration in local search for SAT. In: Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2012, pp. 334–340 (2012)
Cai, S., Su, K.: Local search for Boolean Satisfiability with configuration checking and subscore. Artif. Intell. 204, 75–98 (2013)
Cai, S., Su, K., Sattar, A.: Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artif. Intell. 175(9–10), 1672–1696 (2011)
Fröhlich, A., Biere, A., Wintersteiger, C.M., Hamadi, Y.: Stochastic local search for satisfiability modulo theories. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI 2015, pp. 1136–1143 (2015)
Hutter, F., Tompkins, D.A.D., H. Hoos, H.: Scaling and probabilistic smoothing: efficient dynamic local search for SAT. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 233–248. Springer, Heidelberg (2002)
Li, C.M., Habet, D.: Description of RSeq2014. In: Proc. of SAT Competition 2014: Solver and Benchmark Descriptions, p. 72 (2014)
Li, C.-M., Huang, W.Q.: Diversification and determinism in local search for satisfiability. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 158–172. Springer, Heidelberg (2005)
Li, C.M., Li, Y.: Satisfying versus falsifying in local search for satisfiability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 477–478. Springer, Heidelberg (2012)
Manthey, N.: Coprocessor 2.0 – a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436–441. Springer, Heidelberg (2012)
McAllester, D.A., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: Proceedings of the 14th National Conference on Artificial Intelligence, AAAI 1997, pp. 321–326 (1997)
Morris, P.: The breakout method for escaping from local minima. In: Proceedings of the 11th National Conference on Artificial Intelligence, AAAI 1993, pp. 40–45 (1993)
Papadimitriou, C.H.: On selecting a satisfying truth assignment. In: Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, FOCS 1991, pp. 163–169 (1991)
Pham, D.N., Gretton, C.: gNovelty+. In: Solver Description of SAT Competition 2007 (2007)
Seitz, S., Alava, M., Orponen, P.: Focused local search for random 3-satisfiability. J. Stat. Mech. (2005). P06006
Selman, B., Kautz, H.A.: Domain-independent extensions to gsat: solving large structured satisfiability problems. In: Proceedings of the 13th International Joint Conference on Artificial Intelligence, IJCAI 1993, pp. 290–295 (1993)
Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proceedings of the 12th National Conference on Artificial Intelligence, AAAI 1994, pp. 337–343 (1994)
Thornton, J., Pham, D.N., Bain, S., Jr., V.F.: Additive versus multiplicative clause weighting for SAT. In: Proceedings of the 19th National Conference on Artificial Intelligence, AAAI 2004, pp. 191–196 (2004)
Wu, Z., Wah, B.W.: An efficient global-search strategy in discrete lagrangian methods for solving hard satisfiability problems. In: Proceedings of the 17th National Conference on Artificial Intelligence, AAAI 2000, pp. 310–315 (2000)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Cai, S., Luo, C., Su, K. (2015). CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability. In: Heule, M., Weaver, S. (eds) Theory and Applications of Satisfiability Testing -- SAT 2015. SAT 2015. Lecture Notes in Computer Science(), vol 9340. Springer, Cham. https://doi.org/10.1007/978-3-319-24318-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-24318-4_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24317-7
Online ISBN: 978-3-319-24318-4
eBook Packages: Computer ScienceComputer Science (R0)