Solving SAT in a distributed cloud: A portfolio approach

Ngoko, Yanik ; Cérin, Christophe ; Trystram, Denis

International Journal of Applied Mathematics and Computer Science, Tome 29 (2019) no. 2, pp. 261-274.

Résumé

We introduce a new parallel and distributed algorithm for the solution of the satisfiability problem. It is based on an algorithm portfolio and is intended to be used for servicing requests in a distributed cloud. The core of our contribution is the modeling of the optimal resource sharing schedule in parallel executions and the proposition of heuristics for its approximation. For this purpose, we reformulate a computational problem introduced in a prior work. The main assumption is that it is possible to learn optimal resource sharing from traces collected on past executions on a representative set of instances. We show that the learning can be formalized as a set coverage problem. Then we propose to solve it by approximation and dynamic programming algorithms based on classical greedy algorithms for the maximum coverage problem. Finally, we conduct an experimental evaluation for comparing the performance of the various algorithms proposed. The results show that some algorithms become more competitive if we intend to determine the trade-off between their quality and the runtime required for their computation.

Détail

Keywords: resource provisioning, resource scheduling, parallel distributed SAT, algorithm portfolio, maximum coverage problem
Mots-clés : udostępnianie zasobów, szeregowanie zasobów, problem maksymalnego zasięgu

Bibliographie

[1] Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M. And Piette, C. (2012). PeneLoPe, a parallel clause-freezer solver, SAT Challenge 2012: Solver and Benchmarks Descriptions, Helsinki, Finland, pp. 43–44.

[2] Audemard, G., Hoessen, B., Jabbour, S. and Piette, C. (2014). Dolius: A distributed parallel SAT solving framework, 5th Pragmatics of SAT Workshop POS-14, Vienna, Austria, pp. 1–11.

[3] Biere, A. (2010). Lingeling, plingeling, PicoSAT and PrecoSAT at SAT Race 2010, Technical report, Johannes Kepler University, Linz.

[4] Chrabakh, W. and Wolski, R. (2003). Gridsat: A Chaff-based distributed SAT solver for the grid, Proceedings of the 2003 ACM/IEEE Conference on Supercomputing, SC’03, Phoenix, AZ, USA, pp. 37–50, DOI: 10.1145/1048935.1050188.

[5] Goldman, A., Ngoko, Y. and Trystram, D. (2012). Malleable resource sharing algorithms for cooperative resolution of problems, Congress on Evolutionary Computation World Congress on Computational Intelligence, Brisbane, Australia, pp. 1438–1445.

[6] Hochbaum, D.S. and Pathria, A. (1998). Analysis of the greedy approach in problems of maximum k-coverage, Naval Research Logistics 45(6): 615–627.

[7] Holldobler, S., Manthey, N., Nguyen, V.H., Stecklina, J. And Steinke, P. (2011). A short overview on modern parallel SAT-solvers, 2011 International Conference on Advanced Computer Science and Information System (ICACSIS), Jakarta, Indonesia, pp. 201–206.

[8] Jackson, P. and Sheridan, D. (2005). Clause form conversions for boolean circuits, Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, SAT’04, Vancouver, BC, Canada, pp. 183–198.

[9] Kautz, H. and Selman, B. (2007). The state of SAT, Discrete Applied Mathematics 155(12): 1514–1524.

[10] Martins, R., Manquinho, V. and Lynce, I. (2012). An overview of parallel SAT solving, Constraints 17(3): 304–347.

[11] Ngoko, Y., Saintherant, N., Cérin, C. and Trystram, D. (2018). Invited paper: How future buildings could redefine distributed computing, 2018 IEEE International Parallel and Distributed Processing Symposium Workshops, IPDPS 2018, Vancouver, BC, Canada, pp. 1232–1240.

[12] Ngoko, Y., Trystram, D., Reis, V. and Cérin, C. (2016). An automatic tuning system for solving NP-hard problems in clouds, 2016 IEEE International Parallel and Distributed Processing Symposium Workshops, IPDPS 2016, Chicago, IL, USA, pp. 1443–1452.

[13] Roussel, O. (2011). Description of Ppfolio, https://www.cril.univ-artois.fr/˜roussel/ppfolio/solver1.pdf.

[14] Silva, J.a.P.M. and Sakallah, K.A. (1996). GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM International Conference on Computer-aided Design, ICCAD’96, San Jose, CA, USA, pp. 220–227.

[15] Vardi, M.Y. (2014). Moore’s law and the sand-heap paradox, Communications of the ACM 57(5): 5–5.

[16] Xu, L., Hutter, F., Hoos, H.H. and Leyton-Brown, K. (2008). Satzilla: Portfolio-based algorithm selection for SAT, Journal of Artificial Intelligence Research 32: 565–606.

[17] Zhang, H., Bonacina, M.P. and Hsiang, J. (1996). PSATO: A distributed propositional prover and its application to quasigroup problems, Journal of Symbolic Computation 21(4–6): 543–560.