zbMATH — the first resource for mathematics

Captain Jack: new variable selection heuristics in local search for SAT. (English) Zbl 1330.68277
Sakallah, Karem A. (ed.) et al., Theory and applications of satisfiability testing – SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19–22, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21580-3/pbk). Lecture Notes in Computer Science 6695, 302-316 (2011).
Summary: Stochastic local search (SLS) methods are well known for their ability to find models of randomly generated instances of the propositional satisfiability problem (SAT) very effectively. Two well-known SLS-based SAT solvers are Sparrow, one of the best-performing solvers for random 3-SAT instances, and VE-Sampler, which achieved significant performance improvements over previous SLS solvers on SAT-encoded software verification problems. Here, we introduce a new highly parametric algorithm, Captain Jack, which extends the parameter space of Sparrow to incorporate elements from VE-Sampler and introduces new variable selection heuristics. Captain Jack has a rich design space and can be configured automatically to perform well on various types of SAT instances. We demonstrate that the design space of Captain Jack is easy to interpret and thus facilitates valuable insight into the configurations automatically optimized for different instance sets. We provide evidence that Captain Jack can outperform well-known SLS-based SAT solvers on uniform random \(k\)-SAT and ‘industrial-like’ random instances.
For the entire collection see [Zbl 1215.68023].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
03B05 Classical propositional logic
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Ansótegui, C., Bonet, M.L., Levy, J.: Towards industrial-like random SAT instances. In: IJCAI 2009, pp. 387–392 (2009)
[2] Balint, A., Diepold, D., Gall, D., Gerber, S., Kapler, G., Retz, R.: EDACC - an advanced platform for the experiment design, administration and analysis of empirical algorithms. In: LION-2011 (to appear)
[3] 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) · Zbl 1306.68150 · doi:10.1007/978-3-642-14186-7_3
[4] Biere, A.: PicoSAT essentials. JSAT 4, 75–97 (2008) · Zbl 1159.68403
[5] bwGRiD: Member of the German D-Grid initiative, funded by the Ministry of Education and Research and the Ministry for Science, Research and Arts Baden-Württemberg
[6] Chvátal, V., Szemerédi, E.: Many hard examples for resolution. Journal of the ACM 35(4), 759–768 (1988) · Zbl 0712.03008 · doi:10.1145/48014.48016
[7] Hoos, H.H.: Computer-aided design of high-performance algorithms. Tech. Rep. TR-2008-16, University of British Columbia (2008)
[8] Hutter, F., Hoos, H.H., Leyton-Brown, K., Stützle, T.: ParamILS: An automatic algorithm configuration framework. Journal of Artificial Intelligence Research 36, 267–306 (2009) · Zbl 1192.68831
[9] Hutter, F., Hoos, H.H., Stützle, T.: Automatic algorithm configuration based on local search. In: AAAI 2007, pp. 1152–1157 (2007)
[10] KhudaBukhsh, A.R., Xu, L., Hoos, H.H., Leyton-Brown, K.: SATenstein: Automatically building local search SAT solvers from components. In: IJCAI 2009, pp. 517–524 (2009) · Zbl 1351.68255
[11] 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) · Zbl 1128.68472 · doi:10.1007/11499107_12
[12] Mertens, S., Mézard, M., Zecchina, R.: Threshold values of random k-SAT from the cavity method. Random Structures & Algorithms 28, 340–373 (2006) · Zbl 1094.68035 · doi:10.1002/rsa.20090
[13] Pham, D.N., Thornton, J., Gretton, C., Sattar, A.: Combining adaptive and dynamic local search for satisfiability. JSAT 4, 149–172 (2008) · Zbl 1159.68566
[14] Prestwich, S.: Random walk with continuously smoothed variable weights. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 203–215. Springer, Heidelberg (2005) · Zbl 1128.68478 · doi:10.1007/11499107_15
[15] Thornton, J., Pham, D.N., Bain, S., Ferreira Jr., V.: Using cost distributions to guide weight decay in local search for SAT. In: Ho, T.-B., Zhou, Z.-H. (eds.) PRICAI 2008. LNCS (LNAI), vol. 5351, pp. 405–416. Springer, Heidelberg (2008) · Zbl 05489359 · doi:10.1007/978-3-540-89197-0_38
[16] Tompkins, D.A.D.: Dynamic Local Search for SAT: Design, Insights and Analysis. Ph.D. thesis, University of British Columbia (2010)
[17] Tompkins, D.A.D., Hoos, H.H.: UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306–320. Springer, Heidelberg (2005) · Zbl 1122.68620 · doi:10.1007/11527695_24
[18] Tompkins, D.A.D., Hoos, H.H.: Dynamic scoring functions with variable expressions: New SLS methods for solving SAT. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 278–292. Springer, Heidelberg (2010) · Zbl 1306.68176 · doi:10.1007/978-3-642-14186-7_23
[19] Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: Portfolio-based algorithm selection for SAT. Journal of Artificial Intelligence Research 32, 565–606 (2008) · Zbl 1182.68272
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.