×

SpySMAC: automated configuration and performance analysis of SAT solvers. (English) Zbl 1471.68243

Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 215-222 (2015).
Summary: Most modern SAT solvers expose a range of parameters to allow some customization for improving performance on specific types of instances. Performing this customization manually can be challenging and time-consuming, and as a consequence several automated algorithm configuration methods have been developed for this purpose. Although automatic algorithm configuration has already been applied successfully to many different SAT solvers, a comprehensive analysis of the configuration process is usually not readily available to users. Here, we present SpySMAC to address this gap by providing a lightweight and easy-to-use toolbox for (i) automatic configuration of SAT solvers in different settings, (ii) a thorough performance analysis comparing the best found configuration to the default one, and (iii) an assessment of each parameter’s importance using the fANOVA framework. To showcase our tool, we apply it to Lingeling and probSAT, two state-of-the-art solvers with very different characteristics.
For the entire collection see [Zbl 1323.68009].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ansótegui, C., Sellmann, M., Tierney, K.: A Gender-based genetic algorithm for the automatic configuration of algorithms. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 142–157. Springer, Heidelberg (2009) · Zbl 05612646 · doi:10.1007/978-3-642-04244-7_14
[2] Balint, A., Schöning, U.: Choosing probability distributions for stochastic local search and the role of make versus break. In: Cimatti and Sebastiani [7], pp. 16–19 · Zbl 1273.68333 · doi:10.1007/978-3-642-31612-8_3
[3] Biere, A.: Yet another local search solver and lingeling and friends entering the SAT competition 2014. In: Belov, A., Diepold, D., Heule, M., Järvisalo, M. (eds.) Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2014-2, pp. 39–40. University of Helsinki (2014)
[4] Breimann, L.: Random forests. Machine Learning Journal 45, 5–32 (2001) · Zbl 1007.68152 · doi:10.1023/A:1010933404324
[5] Brochu, E., Cora, V., de Freitas, N.: A tutorial on Bayesian optimization of expensive cost functions, with application to active user modeling and hierarchical reinforcement learning. Computing Research Repository (2010). (CoRR) abs/1012.2599
[6] Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Cimatti and Sebastiani [7], pp. 44–57 · Zbl 1306.68155 · doi:10.1007/978-3-642-14186-7_6
[7] Cimatti, A., Sebastiani, R. (eds.): SAT 2012. LNCS, vol. 7317. Springer, Heidelberg (2012) · Zbl 1268.68009
[8] Fawcett, C., Hoos, H.H.: Analysing differences between algorithm configurations through ablation. Journal of Heuristics, 1–28 (2015)
[9] Gebser, M., Kaufmann, B., Schaub, T.: Conflict-driven answer set solving: From theory to practice. Artificial Intelligence 187–188, 52–89 (2012) · Zbl 1251.68060 · doi:10.1016/j.artint.2012.04.001
[10] Hutter, F., Babić, D., Hoos, H.H., Hu, A.: Boosting verification by automatic tuning of decision procedures. In: O’Conner, L. (ed.) Formal Methods in Computer Aided Design (FMCAD 2007), pp. 27–34. IEEE Computer Society Press (2007) · doi:10.1109/FAMCAD.2007.9
[11] Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 507–523. Springer, Heidelberg (2011) · Zbl 06058615 · doi:10.1007/978-3-642-25566-3_40
[12] Hutter, F., Hoos, H.H., Leyton-Brown, K.: Identifying key algorithm parameters and instance features using forward selection. In: Nicosia, G., Pardalos, P. (eds.) LION 7. LNCS, vol. 7997, pp. 364–381. Springer, Heidelberg (2013) · doi:10.1007/978-3-642-44973-4_40
[13] Hutter, F., Hoos, H.H., Leyton-Brown, K.: An efficient approach for assessing hyperparameter importance. In: Xing, E., Jebara, T. (eds.) Proceedings of the 31th International Conference on Machine Learning, (ICML 2014), vol. 32, pp. 754–762. Omniprdess (2014)
[14] 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
[15] Hutter, F., Lindauer, M., Balint, A., Bayless, S., Hoos, H.H., Leyton-Brown, K.: The Configurable SAT Solver Challenge. Computing Research Repository (CoRR) (2015). http://arxiv.org/abs/1505.01221 · Zbl 1402.68161
[16] KhudaBukhsh, A., Xu, L., Hoos, H.H., Leyton-Brown, K.: SATenstein: automatically building local search SAT solvers from components. In: Boutilier, C. (ed.) Proceedings of the 22th International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 517–524 (2009) · Zbl 1351.68255
[17] López-Ibáñez, M., Dubois-Lacoste, J., Stützle, T., Birattari, M.: The irace package, iterated race for automatic algorithm configuration. Tech. rep., IRIDIA, Université Libre de Bruxelles, Belgium (2011). http://iridia.ulb.ac.be/IridiaTrSeries/IridiaTr2011-004.pdf
[18] Sakallah, K.A., Simon, L. (eds.): SAT 2011. LNCS, vol. 6695, pp. 134–144. Springer, Heidelberg (2011)
[19] Tompkins, D.A.D., Balint, A., Hoos, H.H.: Captain jack: new variable selection heuristics in local search for SAT. In: Sakallah and Simon [18], pp. 302–316 · Zbl 1330.68277 · doi:10.1007/978-3-642-21581-0_24
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.