×

Scalable SAT solving in the cloud. (English) Zbl 07495595

Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 518-534 (2021).
Summary: Previous efforts on making Satisfiability (SAT) solving fit for high performance computing (HPC) have led to super-linear speedups on particular formulae, but for most inputs cannot make efficient use of a large number of processors. Moreover, long latencies (minutes to days) of job scheduling make large-scale SAT solving on demand impractical for most applications. We address both issues with Mallob, a framework for job scheduling in the context of SAT solving which exploits malleability, i.e., the ability to add or remove processing power from a job during its computation. Mallob includes a massively parallel, distributed, and malleable SAT solving engine based on HordeSat with a more succinct and communication-efficient approach to clause sharing and numerous further improvements over its precursor. Experiments with up to 2560 cores show that Mallob outperforms an improved version of HordeSat and scales significantly better. Moreover, Mallob can solve many formulae in parallel while dynamically adapting the assigned resources, and jobs arriving in the system are usually initiated within a fraction of a second.
For the entire collection see [Zbl 1482.68030].

MSC:

68Q25 Analysis of algorithms and problem complexity
68R07 Computational aspects of satisfiability
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Audemard, G., Hoessen, B., Jabbour, S., Piette, C.: Dolius: a distributed parallel SAT solving framework. In: Pragmatics of SAT, pp. 1-11. Citeseer (2014)
[2] Audemard, G.; Lagniez, J-M; Szczepanski, N.; Tabary, S.; Rueher, M., An adaptive parallel SAT solver, Principles and Practice of Constraint Programming, 30-48 (2016), Cham: Springer, Cham
[3] Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Twenty-First International Joint Conference on Artificial Intelligence, pp. 399-404 (2009)
[4] Balyo, T.; Sanders, P.; Sinz, C.; Heule, M.; Weaver, S., HordeSat: a massively parallel portfolio SAT solver, Theory and Applications of Satisfiability Testing - SAT 2015, 156-172 (2015), Cham: Springer, Cham · Zbl 1471.68237
[5] Biere, A.: Yet another local search solver and Lingeling and friends entering the SAT competition 2014. In: Proceedings of SAT Competition, p. 65 (2014)
[6] Biere, A.: Splatz, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT competition 2016. Proceedings of SAT Competition pp. 44-45 (2016)
[7] Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2018. In: Proceedings of SAT Competition, pp. 14-15 (2018)
[8] Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Proceedings of SAT Competition, p. 50 (2020)
[9] Ehlers, T., Nowotka, D., Sieweck, P.: Communication in massively-parallel SAT solving. In: 2014 IEEE 26th International Conference on Tools with Artificial Intelligence, pp. 709-716. IEEE (2014)
[10] Feitelson, DG; Rudolph, L.; Feitelson, DG; Rudolph, L., Toward convergence in job schedulers for parallel supercomputers, Job Scheduling Strategies for Parallel Processing, 1-26 (1996), Heidelberg: Springer, Heidelberg · Zbl 1155.68302
[11] Froleyks, N., Heule, M., Iser, M., Järvisalo, M., Suda, M.: SAT Competition 2020. In: Artificial Intelligence (2021, to appear)
[12] Graham, R.L., Shipman, G.M., Barrett, B.W., Castain, R.H., Bosilca, G., Lumsdaine, A.: Open MPI: a high-performance, heterogeneous MPI. In: 2006 IEEE International Conference on Cluster Computing, pp. 1-9. IEEE (2006)
[13] Gropp, W., Gropp, W.D., Lusk, E., Skjellum, A., Lusk, E.: Using MPI: portable parallel programming with the message-passing interface, vol. 1. MIT Press, Cambridge (1999) · Zbl 0875.68206
[14] Hamadi, Y.; Jabbour, S.; Sais, L., ManySAT: a parallel SAT solver, J. Satisf. Boolean Model. Comput., 6, 4, 245-262 (2010) · Zbl 1193.68227
[15] Heisinger, M.; Fleury, M.; Biere, A.; Pulina, L.; Seidl, M., Distributed cube and conquer with paracooba, Theory and Applications of Satisfiability Testing - SAT 2020, 114-122 (2020), Cham: Springer, Cham · Zbl 07331016
[16] Heule, M., Järvisalo, M., Suda, M.: SAT race 2019 (2019). http://sat-race-2019.ciirc.cvut.cz/downloads/satrace19slides.pdf. Accessed 13 May 2021
[17] Heule, MJH; Kullmann, O.; Wieringa, S.; Biere, A.; Eder, K.; Lourenço, J.; Shehory, O., Cube and conquer: guiding CDCL SAT solvers by Lookaheads, Hardware and Software: Verification and Testing, 50-65 (2012), Heidelberg: Springer, Heidelberg
[18] Hoos, HH; Stützle, T., Local search algorithms for SAT: an empirical evaluation, J. Autom. Reason., 24, 4, 421-481 (2000) · Zbl 0961.68039
[19] Hungershofer, J.: On the combined scheduling of malleable and rigid jobs. In: 16th Symposium on Computer Architecture and High Performance Computing, pp. 206-213. IEEE (2004)
[20] Iser, M., Balyo, T., Sinz, C.: Memory efficient parallel SAT solving with inprocessing. In: 2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI), pp. 64-70. IEEE (2019)
[21] Iser, M.; Sinz, C., A problem meta-data library for research in SAT, Proc. Pragmatics SAT, 59, 144-152 (2019)
[22] Kendall, M.G.: Rank Correlation Methods. Griffin, London (1948)
[23] Kleine Büning, M.; Balyo, T.; Sinz, C.; Ait-Ameur, Y.; Qin, S., Using DimSpec for bounded and unbounded software model checking, Formal Methods and Software Engineering, 19-35 (2019), Cham: Springer, Cham
[24] Le Frioux, L.; Baarir, S.; Sopena, J.; Kordon, F.; Gaspers, S.; Walsh, T., PaInleSS: a framework for parallel SAT solving, Theory and Applications of Satisfiability Testing - SAT 2017, 233-250 (2017), Cham: Springer, Cham · Zbl 06807229
[25] Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131-153 (2009). IOS Press
[26] Massacci, F.; Marraro, L., Logical cryptanalysis as a SAT problem, J. Autom. Reason., 24, 1, 165-203 (2000) · Zbl 0968.68052
[27] Mehlhorn, K., Sanders, P.: Algorithms and data structures: the basic toolbox. Springer Science & Business Media, Berlin (2008). doi:10.1007/978-3-540-77978-0 · Zbl 1146.68069
[28] Ngoko, Y.; Cérin, C.; Trystram, D., Solving SAT in a distributed cloud: a portfolio approach, Int. J. Appl. Math. Comput. Sci., 29, 2, 261-274 (2019) · Zbl 1430.68293
[29] Ngoko, Y., Trystram, D., Cérin, C.: A distributed cloud service for the resolution of SAT. In: 2017 IEEE 7th International Symposium on Cloud and Service Computing (SC2), pp. 1-8. IEEE (2017)
[30] Schreiber, D., Lilotane: a lifted SAT-based approach to hierarchical planning, J. Artif. Intell. Res., 70, 1117-1181 (2021) · Zbl 07328103
[31] Schubert, T.; Lewis, M.; Becker, B., PaMiraXT: parallel SAT solving with threads and message passing, J. Satisfiability, Boolean Model. Comput., 6, 4, 203-222 (2010) · Zbl 1190.68057
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.