×

zbMATH — the first resource for mathematics

Automatic construction of parallel portfolios via algorithm configuration. (English) Zbl 1404.68144
Summary: Since 2004, increases in computational power described by Moore’s law have substantially been realized in the form of additional cores rather than through faster clock speeds. To make effective use of modern hardware when solving hard computational problems, it is therefore necessary to employ parallel solution strategies. In this work, we demonstrate how effective parallel solvers for propositional satisfiability (SAT), one of the most widely studied NP-complete problems, can be produced automatically from any existing sequential, highly parametric SAT solver. Our Automatic Construction of Parallel Portfolios (ACPP) approach uses an automatic algorithm configuration procedure to identify a set of configurations that perform well when executed in parallel. Applied to two prominent SAT solvers, Lingeling and clasp, our ACPP procedure identified 8-core solvers that significantly outperformed their sequential counterparts on a diverse set of instances from the application and hard combinatorial category of the 2012 SAT Challenge. We further extended our ACPP approach to produce parallel portfolio solvers consisting of several different solvers by combining their configuration spaces. Applied to the component solvers of the 2012 SAT Challenge gold medal winning SAT Solver pfolioUZK, our ACPP procedures produced a significantly better-performing parallel SAT solver.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68W01 General topics in the theory of algorithms
68W10 Parallel algorithms in computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aigner, M.; Biere, A.; Kirsch, C.; Niemetz, A.; Preiner, M., Analysis of portfolio-style parallel SAT solving on current multi-core architectures, (Proceedings of the Fourth International Workshop on Pragmatics of SAT, POS’13, (2013))
[2] Amadini, R.; Gabbrielli, M.; Mauro, J., A multicore tool for constraint solving, (Yang, Q.; Wooldridge, M., Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI’15, (2015), AAAI Press), 232-238
[3] 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
[4] Asin, R.; Olate, J.; Ferres, L., Cache performance study of portfolio-based parallel CDCL SAT solvers, (2013), CoRR
[5] G. Audemard, B. Hoessen, S. Jabbour, J.-M. Lagniez, C. Piette, Penelope, a parallel clause-freezer solver, in: [7], pp. 43-44, available at https://helda.helsinki.fi/handle/10138/34218.
[6] G. Audemard, L. Simon, GLUCOSE 2.1 in the SAT Challenge 2012, in: [7], p. 21, available at https://helda.helsinki.fi/handle/10138/34218.
[7] (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), available at
[8] (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)
[9] Balyo, T.; Sanders, P.; Sinz, C., Hordesat: a massively parallel portfolio SAT solver, (Heule, M.; Weaver, S., Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, SAT’15, Lecture Notes in Computer Science, vol. 9340, (2015), Springer-Verlag), 156-172 · Zbl 06512571
[10] Baral, C., Knowledge representation, reasoning and declarative problem solving, (2003), Cambridge University Press · Zbl 1056.68139
[11] (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-2012-2, (2014), University of Helsinki)
[12] Biere, A., Lingeling, plingeling, picosat and precosat at SAT race 2010, (2010), Institute for Formal Models and Verification, Johannes Kepler University, Tech. Rep. 10/1
[13] Biere, A., Lingeling and friends at the SAT competition 2011, (2011), Institute for Formal Models and Verification, Johannes Kepler University, Technical Report FMV 11/1
[14] A. Biere, Lingeling and friends entering the SAT Challenge 2012, in: [7], pp. 33-34, available at https://helda.helsinki.fi/handle/10138/34218.
[15] A. Biere, Lingeling, plingeling and treengeling entering the SAT Competition 2013, in: [8], pp. 51-52.
[16] A. Biere, Yet another local search solver and lingeling and friends entering the SAT Competition 2014, in: [11], pp. 39-40.
[17] (Boutilier, C., Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence, IJCAI’09, (2009), AAAI/MIT Press)
[18] S. Cai, C. Luo, K. Su, CCASAT: solver description, in: [7], pp. 13-14, available at https://helda.helsinki.fi/handle/10138/34218.
[19] Chen, J., Phase selection heuristics for satisfiability solvers, (2011), CoRR
[20] (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
[21] Eén, N.; Biere, A., Effective preprocessing in SAT through variable and clause elimination, (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-Verlag), 61-75 · Zbl 1128.68463
[22] 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, (2004), Springer-Verlag), 502-518 · Zbl 1204.68191
[23] G. Audemard, B.H. Jabbour, J. Lagniez, C. Piette, PeneLoPe in SAT Competition 2014, in: [11], pp. 58-59.
[24] Gagliolo, M.; Schmidhuber, J., Learning dynamic algorithm portfolios, Ann. Math. Artif. Intell., 47, 3-4, 295-328, (2006) · Zbl 1113.68101
[25] Gebser, M.; Kaminski, R.; Kaufmann, B.; Schaub, T., Answer set solving in practice. synthesis lectures on artificial intelligence and machine learning, (2012), Morgan and Claypool Publishers
[26] Gebser, M.; Kaufmann, B.; Schaub, T., Multi-threaded ASP solving with clasp, Theory Pract. Log. Program., 12, 4-5, 525-545, (2012) · Zbl 1260.68061
[27] Gomes, C.; Selman, B., Algorithm portfolios, Artif. Intell., 126, 1-2, 43-62, (2001) · Zbl 0969.68047
[28] A. Grinten, A. Wotzlaw, E. Speckenmeyer, S. Porschen, satUZK: solver description, in: [7], pp. 54-55, available at https://helda.helsinki.fi/handle/10138/34218.
[29] Guo, L.; Hamadi, Y.; Jabbour, S.; Sais, L., Diversification and intensification in parallel SAT solving, (Cohen, D., Proceedings of the Sixteenth International Conference on Principles and Practice of Constraint Programming, CP’10, Lecture Notes in Computer Science, vol. 6308, (2010), Springer-Verlag), 252-265
[30] Y. Hamadi, S. Jabbour, L. Sais, Control-based clause sharing in parallel SAT solving, in: [17], pp. 499-504.
[31] Hamadi, Y.; Jabbour, S.; Sais, L., Manysat: a parallel SAT solver, J. Satisf. Boolean Model. Comput., 6, 245-262, (2009) · Zbl 1193.68227
[32] Hamadi, Y.; Wintersteiger, C., Seven challenges in parallel SAT solving, AI Mag., 34, 99-106, (2013)
[33] Heule, M.; Dufour, M.; van Zwieten, J.; van Maaren, H., March_eq: implementing additional reasoning into an efficient look-ahead SAT solver, (Hoos, H.; Mitchell, D., Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing, SAT’04, Lecture Notes in Computer Science, vol. 3542, (2004), Springer-Verlag), 345-359 · Zbl 1122.68599
[34] Hoos, H., Programming by optimisation, Commun. ACM, 55, 70-80, (2012)
[35] Hoos, H.; Kaminski, R.; Schaub, T.; Schneider, M., Aspeed: ASP-based solver scheduling, (Dovier, A.; Santos Costa, V., Technical Communications of the Twenty-Eighth International Conference on Logic Programming, ICLP’12, Leibniz International Proceedings in Informatics (LIPIcs), vol. 17, (2012)), 176-187 · Zbl 1281.68206
[36] Hoos, H.; Kaufmann, B.; Schaub, T.; Schneider, M., Robust benchmark set selection for Boolean constraint solvers, (Pardalos, P.; Nicosia, G., Proceedings of the Seventh International Conference on Learning and Intelligent Optimization, LION’13, Lecture Notes in Computer Science, vol. 7997, (2013), Springer-Verlag), 138-152
[37] Hoos, H.; Leyton-Brown, K.; Schaub, T.; Schneider, M., Algorithm configuration for portfolio-based parallel SAT-solving, (Coletta, R.; Guns, T.; O’Sullivan, B.; Passerini, A.; Tack, G., Proceedings of the First Workshop on Combining Constraint Solving with Mining and Learning, CoCoMile’12, (2012)), 7-12
[38] Hoos, H.; Stützle, T., Stochastic local search: foundations and applications, (2004), Elsevier/Morgan Kaufmann · Zbl 1126.68032
[39] Huberman, B.; Lukose, R.; Hogg, T., An economic approach to hard computational problems, Science, 275, 51-54, (1997)
[40] Hutter, F.; Hoos, H.; Leyton-Brown, K., Sequential model-based optimization for general algorithm configuration, (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
[41] Hutter, F.; Hoos, H.; Leyton-Brown, K., Submodular configuration of algorithms for portfolio-based selection, (2014), Department of Computer Science, University of British Columbia, in press
[42] 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
[43] Hutter, F.; López-Ibáñez, M.; Fawcett, C.; Lindauer, M.; Hoos, H.; Leyton-Brown, K.; Stützle, T., Aclib: a benchmark library for algorithm configuration, (Pardalos, P.; Resende, M.; Vogiatzis, C.; Walteros, J., Proceedings of the Eigth International Conference on Learning and Intelligent Optimization, LION’14, Lecture Notes in Computer Science, vol. 8426, (2014), Springer-Verlag), 36-40
[44] 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
[45] Kadioglu, S.; Malitsky, Y.; Sellmann, M.; Tierney, K., ISAC - instance-specific algorithm configuration, (Coelho, H.; Studer, R.; Wooldridge, M., Proceedings of the Nineteenth European Conference on Artificial Intelligence, ECAI’10, (2010), IOS Press), 751-756
[46] Katsirelos, G.; Sabharwal, A.; Samulowitz, H.; Simon, L., Resolution and parallelizability: barriers to the efficient parallelization of SAT solvers, (desJardins, M.; Littman, M., Proceedings of the Twenty-Seventh National Conference on Artificial Intelligence, AAAI’13, (2013), AAAI Press)
[47] A. KhudaBukhsh, L. Xu, F. Hutter, H. Hoos, K. Leyton-Brown, SATenstein: automatically building local search SAT solvers from components, in: [17], pp. 517-524. · Zbl 1351.68255
[48] Kotthoff, L., Algorithm selection for combinatorial search problems: a survey, (2012), University College Cork, Tech. rep.
[49] Lazaar, N.; Hamadi, Y.; Jabbour, S.; Sebag, M., Cooperation control in parallel SAT solving: a multi-armed bandit approach, (2012), INRIA, Tech. rep.
[50] C. Li, W. Wei, Y. Li, Exploiting historical relationships of clauses and variables in local search for satisfiability, in: [20], pp. 479-480.
[51] Lindauer, M.; Hoos, H.; Hutter, F., From sequential algorithm selection to parallel portfolio selection, (Proceedings of the International Conference on Learning and Intelligent Optimization, LION’15, (2015)), 1-16
[52] 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, Tech. rep.
[53] Malitsky, Y.; Sabharwal, A.; Samulowitz, H.; Sellmann, M., Parallel SAT solver selection and scheduling, (Milano, M., Proceedings of the Eighteenth International Conference on Principles and Practice of Constraint Programming, CP’12, Lecture Notes in Computer Science, vol. 7514, (2012), Springer-Verlag), 512-526
[54] Malitsky, Y.; Sabharwal, A.; Samulowitz, H.; Sellmann, M., Algorithm portfolios based on cost-sensitive hierarchical clustering, (Rossi, F., Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI’13, (2013), IJCAI/AAAI), 608-614
[55] Y. Malitsky, A. Sabharwal, H. Samulowitz, M. Sellmann, Parallel lingeling, ccasat, and csch-based portfolio, in: [8], pp. 26-27.
[56] Malitsky, Y.; Sellmann, M., Instance-specific algorithm configuration as a method for non-model-based portfolio generation, (Beldiceanu, N.; Jussien, N.; Pinson, E., CPAIOR, Lecture Notes in Computer Science, vol. 7298, (2012), Springer-Verlag), 244-259
[57] Moskewicz, M.; Madigan, C.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient SAT solver, (Proceedings of the Thirty-Eighth Conference on Design Automation, DAC’01, (2001), ACM Press), 530-535
[58] E. Nudelman, K. Leyton-Brown, G. Andrew, C. Gomes, J. McFadden, B. Selman, Y. Shoham, Satzilla 0.9, solver description, International SAT Competition, 2003.
[59] S. Núnez, D. Borrajo, C. López, Mipsat, in: [8], pp. 59-60.
[60] O’Mahony, E.; Hebrard, E.; Holland, A.; Nugent, C.; O’Sullivan, B., Using case-based reasoning in an algorithm portfolio for constraint solving, (Bridge, D.; Brown, K.; O’Sullivan, B.; Sorensen, H., Proceedings of the Nineteenth Irish Conference on Artificial Intelligence and Cognitive Science, AICS’08, (2008))
[61] Papadimitriou, C.; Steiglitz, K., Combinatorial optimization: algorithms and complexity, (1982), Prentice-Hall Upper Saddle River, NJ, USA · Zbl 0503.90060
[62] Petrik, M.; Zilberstein, S., Learning static parallel portfolios of algorithms, (Proceedings of the International Symposium on Artificial Intelligence and Mathematics, ISAIM 2006, (2006)) · Zbl 1121.68095
[63] Roussel, O., Description of ppfolio, (2011), available at
[64] Schrijver, A., Theory of linear and integer programming, (1986), John Wiley & Sons New York, NY, USA · Zbl 0665.90063
[65] Soos, M.; Nohl, K.; Castelluccia, C., Extending SAT solvers to cryptographic problems, (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-Verlag), 244-257
[66] Thornton, C.; Hutter, F.; Hoos, H.; Leyton-Brown, K., Auto-WEKA: combined selection and hyperparameter optimization of classification algorithms, (Proceedings of the 19th International Conference on Knowledge Discovery and Data Mining, KDD’13, (2013)), 847-855
[67] Tompkins, D.; Balint, A.; Hoos, H., Captain Jack - new variable selection heuristics in local search for SAT, (Sakallah, K.; 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-Verlag), 302-316 · Zbl 1330.68277
[68] van Gelder, A., Contrast - a Contrarian SAT solver, J. Satisf. Boolean Model. Comput., 8, 1/2, 117-122, (2012) · Zbl 1322.68188
[69] Wei, W.; Li, C., Switching between two adaptive noise mechanism in local search for SAT, (2009), available at
[70] A. Wotzlaw, A. van der Grinten, E. Speckenmeyer, S. Porschen, pfolioUZK: solver description, in: [7], p. 45, available at https://helda.helsinki.fi/handle/10138/34218.
[71] Xu, L.; Hoos, H.; Leyton-Brown, K., Hydra: automatically configuring algorithms for portfolio-based selection, (Fox, M.; Poole, D., Proceedings of the Twenty-Fourth National Conference on Artificial Intelligence, AAAI’10, (2010), AAAI Press), 210-216
[72] 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
[73] L. Xu, F. Hutter, H. Hoos, K. Leyton-Brown, Evaluating component solver contributions to portfolio-based algorithm selectors, in: [20], pp. 228-241.
[74] L. Xu, F. Hutter, J. Shen, H. Hoos, K. Leyton-Brown, SATzilla2012: improved algorithm selection based on cost-sensitive classification models, in: [7], pp. 57-58, available at https://helda.helsinki.fi/handle/10138/34218.
[75] T. Yasumoto, Sinn, in: A. Balint, A. Belov, D. Diepold, S. Gerber, M. Järvisalo, C. Sinz (Eds.), Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, in: [7], pp. 61-61, available at https://helda.helsinki.fi/handle/10138/34218.
[76] Yun, X.; Epstein, S., Learning algorithm portfolios for parallel execution, (Hamadi, Y.; Schoenauer, M., Proceedings of the Sixth International Conference Learning and Intelligent Optimization, LION’12, Lecture Notes in Computer Science, vol. 7219, (2012), Springer-Verlag), 323-338
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.