×

The configurable SAT solver challenge (CSSC). (English) Zbl 1402.68161

Summary: It is well known that different solution strategies work well for different types of instances of hard combinatorial problems. As a consequence, most solvers for the propositional satisfiability problem (SAT) expose parameters that allow them to be customized to a particular family of instances. In the international SAT competition series, these parameters are ignored: solvers are run using a single default parameter setting (supplied by the authors) for all benchmark instances in a given track. While this competition format rewards solvers with robust default settings, it does not reflect the situation faced by a practitioner who only cares about performance on one particular application and can invest some time into tuning solver parameters for this application. The new Configurable SAT Solver Competition (CSSC) compares solvers in this latter setting, scoring each solver by the performance it achieved after a fully automated configuration step. This article describes the CSSC in more detail, and reports the results obtained in its two instantiations so far, CSSC 2013 and 2014.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Ansótegui, C.; Sellmann, M.; Tierney, K., A gender-based genetic algorithm for the automatic configuration of algorithms, (Gent, I., Proceedings of the Fifteenth International Conference on Principles and Practice of Constraint Programming, CP’09, Lecture Notes in Computer Science, vol. 5732, (2009), Springer-Verlag), 142-157
[2] G. Audemard, L. Simon, Predicting learnt clauses quality in modern SAT solvers, in: [21], 2009, pp. 399-404.
[3] Babić, D.; Hu, A., Structural abstraction of software verification conditions, (Damm, W.; Hermanns, H., Proceedings of the International Conference on Computer Aided Verification, CAV’07, Lecture Notes in Computer Science, vol. 4590, (2007), Springer), 366-378 · Zbl 1135.68463
[4] Babić, D.; Hu, A. J., Exploiting shared structure in software verification conditions, (Yorav, K., Proceedings of the International Conference on Hardware and Software: Verification and Testing, HVC’08, Lecture Notes in Computer Science, vol. 4899, (2008), Springer), 169-184
[5] D. Babić, F. Hutter, Spear theorem prover. Solver description, SAT competition, 2007.
[6] V. Balabanov, Solver43, in: [7], 2013, p. 86.
[7] (Balint, A.; Belov, A.; Heule, M.; Järvisalo, M., Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, vol. B-2013-1, (2013), University of Helsinki)
[8] A. Balint, N. Manthey, SparrowToRiss, in: [13], 2014, pp. 77-78.
[9] A. Balint, U. Schöning, Choosing probability distributions for stochastic local search and the role of make versus break, in: [25], 2012, pp. 16-29. · Zbl 1273.68333
[10] Bayardo, R. J.; Schrag, R., Using CSP look-back techniques to solve real-world SAT instances, (Kuipers, B.; Webber, B., Proceedings of the Fourteenth National Conference on Artificial Intelligence, AAAI’97, (1997), AAAI Press), 203-208
[11] Bayless, S.; Tompkins, D.; Hoos, H., Evaluating instance generators by configuration, (Pardalos, P.; Resende, M., Proceedings of the Eighth International Conference on Learning and Intelligent Optimization, LION’14, Lecture Notes in Computer Science, (2014), Springer-Verlag)
[12] J. Bebel, H. Yuen, Hard SAT instances based on factoring, in: [7], 2013, p. 102.
[13] (Belov, A.; Diepold, D.; Heule, M.; Järvisalo, M., Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, vol. B-2014-2, (2014), University of Helsinki)
[14] Berre, D. L.; Parrain, A., The sat4j library, release 2.2, system description, J. Satisf. Boolean Model. Comput., 7, 59-64, (2010)
[15] Biere, A., The AIGER and-inverter graph (AIG) format, (2007), Available at
[16] A. Biere, Lingeling, plingeling and treengeling entering the SAT competition 2013, in: [7], 2013, pp. 51-52.
[17] A. Biere, Yet another local search solver and Lingeling and friends entering the SAT competition 2014, in: [13], 2014, pp. 39-40.
[18] Biere, A.; Cimatti, A.; Claessen, K. L.; Jussila, T.; McMillan, K.; Somenzi, F., Benchmarks from the 2008 hardware model checking competition (HWMCC’08), (2008), Available at
[19] Biere, A.; Cimatti, A.; Clarke, E.; Fujita, M.; Zhu, Y., Symbolic model checking using SAT procedures instead of bdds, (Proceedings of Design Automation Conference, DAC’99, (1999)), 317-320
[20] Biere, A.; Le Berre, D.; Lonca, E.; Manthey, N., Detecting cardinality constraints in CNF, (Sinz, C.; Egly, U., Proceedings of the Seventeenth International Conference on Theory and Applications of Satisfiability Testing, SAT’14, Lecture Notes in Computer Science, vol. 8561, (2014), Springer-Verlag), 285-301 · Zbl 1423.68437
[21] (Boutilier, C., Proceedings of the 22th International Joint Conference on Artificial Intelligence, IJCAI’09, (2009))
[22] Breimann, L., Random forests, J. Mach. Learn. Res., 45, 5-32, (2001)
[23] R. Brummayer, F. Lonsing, A. Biere, Automated testing and debugging of SAT and QBF solvers, in: [25], 2012, pp. 44-57. · Zbl 1306.68155
[24] Cadar, C.; Dunbar, D.; Engler, D. R., Klee: unassisted and automatic generation of high-coverage tests for complex systems programs, (Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI’08, vol. 8, (2008)), 209-224
[25] (Cimatti, A.; Sebastiani, R., Proceedings of the Fifteenth International Conference on Theory and Applications of Satisfiability Testing, SAT’12, Lecture Notes in Computer Science, vol. 7317, (2012), Springer-Verlag) · Zbl 1268.68009
[26] Clarke, E.; Kroening, D.; Lerda, F., A tool for checking ANSI-C programs, (Tools and Algorithms for the Construction and Analysis of Systems, (2004), Springer), 168-176 · Zbl 1126.68470
[27] Cook, S., The complexity of theorem proving procedures, (Harrison, M.; Banerji, R.; Ullman, J., Proceedings of the Third Annual ACM Symposium on the Theory of Computing, STOC’71, (1971), ACM), 151-158
[28] Crawford, J.; Baker, A., Experimental results on the application of satisfiability algorithms to scheduling problems, (Proceedings of the National Conference on Artificial Intelligence, AAAI’94, (1994), AAAI Press/MIT Press), 1092-1097
[29] T.-T. Duong, D.-N. Pham, gNovelty+GC: weight-enhanced diversification on stochastic local search for SAT, in: [7], 2013, pp. 49-50.
[30] Eén, N.; Sörensson, N., An extensible SAT-solver, (Giunchiglia, E.; Tacchella, A., Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing, SAT’03, Lecture Notes in Computer Science, vol. 2919, (2003), Springer), 502-518 · Zbl 1204.68191
[31] Fern, A.; Khardon, R.; Tadepalli, P., The first learning track of the international planning competition, Mach. Learn., 84, 1-2, 81-107, (2011)
[32] Feurer, M.; Klein, A.; Eggensperger, K.; Springenberg, J. T.; Blum, M.; Hutter, F., Efficient and robust automated machine learning, (Cortes, C.; Lawrence, N.; Lee, D.; Sugiyama, M.; Garnett, R., Proceedings of the 29th International Conference on Advances in Neural Information Processing Systems, NIPS’15, (2015))
[33] Gebser, M.; Kaufmann, B.; Schaub, T., Conflict-driven answer set solving: from theory to practice, Artif. Intell., 187-188, 52-89, (2012) · Zbl 1251.68060
[34] Gelder, A. V., Toward leaner binary-clause reasoning in a satisfiability solver, Ann. Math. Artif. Intell., 43, 1, 239-253, (2005) · Zbl 1099.68097
[35] Gomes, C.; Selman, B.; Crato, N.; Kautz, H., Heavy-tailed phenomena in satisfiability and constraint satisfaction problems, J. Autom. Reason., 24, 1-2, 67-100, (2000) · Zbl 0967.68145
[36] Han, C.-S.; Jiang, J.-H., Simpsat 1.0 for sat challenge 2012, (Balint, A.; Belov, A.; Diepold, D.; Gerber, S.; Järvisalo, M.; Sinz, C., Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, vol. B-2012-2, (2012), University of Helsinki), 59
[37] Han, C.-S.; Jiang, J.-H., When Boolean satisfiability meets Gaussian elimination in a simplex way, (Computer Aided Verification, (2012)), 410-426
[38] H. Han, F. Somenzi, On-the-fly clause improvement, in: [56], 2009, pp. 209-222.
[39] M.J. Heule, M. Järvisalo, A. Biere, Efficient CNF simplification based on binary implication graphs, in: [74], 2011, pp. 201-215. · Zbl 1330.68269
[40] Hoos, H.; Stützle, T., Stochastic local search: foundations & applications, (2004), Morgan Kaufmann Publishers Inc. San Francisco, CA, USA · Zbl 1126.68032
[41] Hoos, H. H., Programming by optimization, Commun. ACM, 55, 2, 70-80, (2012)
[42] Hutter, F.; Babić, D.; Hoos, H.; Hu, A., Boosting verification by automatic tuning of decision procedures, (O’Conner, L., Formal Methods in Computer Aided Design, FMCAD’07, (2007), IEEE Computer Society Press), 27-34
[43] Hutter, F.; Balint, A.; Bayless, S.; Hoos, H.; Leyton-Brown, K., Results of the configurable SAT solver challenge 2013, (2014), University of Freiburg, Department of Computer Science, Technical report 276
[44] Hutter, F.; Hoos, H.; Leyton-Brown, K., Tradeoffs in the empirical evaluation of competing algorithm designs, Special Issue on Learning and Intelligent Optimization, Ann. Math. Artif. Intell., 60, 1, 65-89, (2010)
[45] Hutter, F.; Hoos, H.; Leyton-Brown, K., Bayesian optimization with censored response data, (NIPS Workshop on Bayesian Optimization, Sequential Experimental Design, and Bandits, (2011)), Published online
[46] Hutter, F.; Hoos, H.; Leyton-Brown, K., Sequential model-based optimization for general algorithm configuration, (Coello, C., Proceedings of the Fifth International Conference on Learning and Intelligent Optimization, LION’11, Lecture Notes in Computer Science, vol. 6683, (2011), Springer-Verlag), 507-523
[47] Hutter, F.; Hoos, H.; Leyton-Brown, K.; Stützle, T., Paramils: an automatic algorithm configuration framework, J. Artif. Intell. Res., 36, 267-306, (2009) · Zbl 1192.68831
[48] Hutter, F.; Lindauer, M.; Bayless, S.; Hoos, H.; Leyton-Brown, K., Results of the configurable SAT solver challenge 2014, (2014), University of Freiburg, Department of Computer Science, Technical report 277
[49] Hutter, F.; Xu, L.; Hoos, H.; Leyton-Brown, K., Algorithm runtime prediction: methods and evaluation, Artif. Intell., 206, 79-111, (2014) · Zbl 1334.68185
[50] Järvisalo, M.; Berre, D. L.; Roussel, O.; Simon, L., The international SAT solver competitions, AI Mag., 33, 1, (2012)
[51] Järvisalo, M.; Biere, A.; Heule, M. J., Blocked clause elimination, (Esparza, J.; Majumdar, R., Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 6015, (2010), Springer Berlin, Heidelberg), 129-144 · Zbl 1284.03208
[52] Kadioglu, S.; Malitsky, Y.; Sabharwal, A.; Samulowitz, H.; Sellmann, M., Algorithm selection and scheduling, (Lee, J., Proceedings of the Seventeenth International Conference on Principles and Practice of Constraint Programming, CP’11, Lecture Notes in Computer Science, vol. 6876, (2011), Springer-Verlag), 454-469
[53] Kautz, H.; Selman, B., Pushing the envelope: planning, propositional logic, and stochastic search, (Shrobe, H.; Senator, T., Proceedings of the Fourteenth National Conference on Artificial Intelligence, AAAI’96, (1996), AAAI Press), 1194-1201
[54] H. Kautz, B. Selman, Unifying SAT-based and graph-based planning, in: [13], 2014, pp. 318-325.
[55] A. KhudaBukhsh, L. Xu, H. Hoos, K. Leyton-Brown, SATenstein: automatically building local search SAT solvers from components, in: [21], 2009, pp. 517-524. · Zbl 1351.68255
[56] (Kullmann, O., Proceedings of the Twelfth International Conference on Theory and Applications of Satisfiability Testing, SAT’09, Lecture Notes in Computer Science, vol. 5584, (2009), Springer)
[57] López-Ibáñez, M.; Dubois-Lacoste, J.; Stützle, T.; Birattari, M., The irace package, iterated race for automatic algorithm configuration, (2011), IRIDIA, Université Libre de Bruxelles Belgium, Technical report
[58] Lourenço, H.; Martin, O.; Stützle, T., Iterated local search, (Handbook of Metaheuristics, (2003), Springer New York), 321-353 · Zbl 1116.90412
[59] Luo, C.; Cai, S.; Wu, W.; Su, K., Focused random walk with configuration checking and break minimum for satisfiability, (Bessiere, C., Proceedings of the Ninth International Conference on Principles and Practice of Constraint Programming, CP’13, Lecture Notes in Computer Science, vol. 4741, (2012), Springer-Verlag), 481-496
[60] Luo, C.; Cai, S.; Wu, W.; Su, K., Double configuration checking in stochastic local search for satisfiability, (Brodley, C.; Stone, P., Proceedings of the Twenty-Eighth National Conference on Artificial Intelligence, AAAI’14, (2014), AAAI Press), 2703-2709
[61] Lynce, I.; Marques-Silva, J. P., Probing-based preprocessing techniques for propositional satisfiability, (15th IEEE International Conference on Tools with Artificial Intelligence, (2003), IEEE Computer Society), 105-110
[62] N. Manthey, Coprocessor 2.0 - a flexible CNF simplifier, in: [25], 2012, pp. 436-441.
[63] N. Manthey, The SAT solver RISS3G at SC 2013, in: [7], 2013, pp. 72-73.
[64] N. Manthey, Riss 4.27, in: [13], 2014, pp. 65-67.
[65] Manthey, N.; Heule, M. J.; Biere, A., Automated reencoding of Boolean formulas, (Biere, A.; Nahir, A.; Vos, T., Hardware and Software: Verification and Testing, Lecture Notes in Computer Science, vol. 7857, (2013), Springer Berlin, Heidelberg), 102-117
[66] Manthey, N.; Philipp, T., Formula simplifications as DRAT derivations, (Lutz, C.; Tielscher, M., KI 2014: Advances in Artificial Intelligence, Lecture Notes in Computer Science, vol. 8736, (2014), Springer Berlin, Heidelberg), 111-122
[67] N. Manthey, P. Steinke, Too many rooks, in: [13], 2014, pp. 97-98.
[68] F. Mugrauer, A. Balint, SAT encoded graph isomorphism benchmark description, in: [7], 2013.
[69] F. Mugrauer, A. Balint, SAT encoded low autocorrelation binary sequence (labs) benchmark description, in: [7], 2013.
[70] Nudelman, E.; Leyton-Brown, K.; Hoos, H. H.; Devkar, A.; Shoham, Y., Understanding random SAT: beyond the clauses-to-variables ratio, (Wallace, M., Proceedings of the Tenth International Conference on Principles and Practice of Constraint Programming, CP’04, Lecture Notes in Computer Science, vol. 3258, (2004), Springer-Verlag), 438-452 · Zbl 1152.68569
[71] C. Oh, Minisat hack 999ed, minisat hack 1430ed and swdia5by, in: [13], 2014, p. 46.
[72] Prasad, M.; Biere, A.; Gupta, A., A survey of recent advances in SAT-based formal verification, Int. J. Softw. Tools Technol. Transf., 7, 2, 156-173, (2005)
[73] Roussel, O., Controlling a solver execution with the runsolver tool, J. Satisf. Boolean Model. Comput., 7, 4, 139-144, (2011) · Zbl 1331.68210
[74] (Sakallah, K. A.; Simon, L., Proceedings of the Fourteenth International Conference on Theory and Applications of Satisfiability Testing, SAT’11, Lecture Notes in Computer Science, vol. 6695, (2011), Springer)
[75] J. Seipp, S. Sievers, F. Hutter, Fast downward SMAC. Planner abstract, IPC 2014 Planning and Learning Track, 2014.
[76] Simon, L.; Berre, D. L.; Hirsch, E., The SAT2002 competition report, Ann. Math. Artif. Intell., 43, 307-342, (2005)
[77] M. Soos, CryptoMiniSat v4, in: [13], 2014, p. 23.
[78] M. Soos, K. Nohl, C. Castelluccia, Extending SAT solvers to cryptographic problems, in: [56], 2009, pp. 244-257.
[79] Stephan, P.; Brayton, R.; Sangiovanni-Vencentelli, A., Combinational test generation using satisfiability, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 15, 1167-1176, (1996)
[80] Thornton, C.; Hutter, F.; Hoos, H.; Leyton-Brown, K., Auto-WEKA: combined selection and hyperparameter optimization of classification algorithms, (Dhillon, I.; Koren, Y.; Ghani, R.; Senator, T.; Bradley, P.; Parekh, R.; He, J.; Grossman, R.; Uthurusamy, R., The 19th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD’13, (2013), ACM Press), 847-855
[81] D. Tompkins, A. Balint, H. Hoos, Captain jack: new variable selection heuristics in local search for SAT, in: [74], 2011, pp. 302-316. · Zbl 1330.68277
[82] Torán, J., On the resolution complexity of graph non-isomorphism, (Järvisalo, M.; Van Gelder, A., Proceedings of the Sixteenth International Conference on Theory and Applications of Satisfiability Testing, SAT’13, Lecture Notes in Computer Science, vol. 7962, (2013), Springer-Verlag), 52-66 · Zbl 1433.03139
[83] van Gelder, A., Another look at graph coloring via propositional satisfiability, (Proceedings of Computational Symposium on Graph Coloring and Generalizations, COLOR-02, (2002)), 48-54
[84] Xu, L.; Hutter, F.; Hoos, H.; Leyton-Brown, K., Satzilla: portfolio-based algorithm selection for SAT, J. Artif. Intell. Res., 32, 565-606, (2008) · Zbl 1182.68272
[85] Zarpas, E., Benchmarking SAT solvers for bounded model checking, (Bacchus, F.; Walsh, T., Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing, SAT’05, Lecture Notes in Computer Science, vol. 3569, (2005), Springer), 340-354 · Zbl 1128.68368
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.