×

Solving SAT in a distributed cloud: a portfolio approach. (English) Zbl 1430.68293

Summary: 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.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68W15 Distributed algorithms
68W25 Approximation algorithms
PDFBibTeX XMLCite
Full Text: DOI

References:

[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 Logistics45(6): 615-627.; · Zbl 0938.90026
[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.; · Zbl 1122.68603
[9] Kautz, H. and Selman, B. (2007). The state of SAT, Discrete Applied Mathematics155(12): 1514-1524.; · Zbl 1121.68108
[10] Martins, R., Manquinho, V. and Lynce, I. (2012). An overview of parallel SAT solving, Constraints17(3): 304-347.; · Zbl 1309.90057
[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, .;
[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 ACM57(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 Research32: 565-606.; · Zbl 1182.68272
[17] Zhang, H., Bonacina, M.P. and Hsiang, J. (1996). PSATO: A distributed propositional prover and its application to quasigroup problems, Journal of Symbolic Computation21(4-6): 543-560.; · Zbl 0863.68013
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.