Distributed cube and conquer with Paracooba. (English) Zbl 07331016

Pulina, Luca (ed.) et al., Theory and applications of satisfiability testing – SAT 2020. 23rd international conference, Alghero, Italy, July 3–10, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12178, 114-122 (2020).
Summary: Cube and conquer is currently the most effective approach to solve hard combinatorial problems in parallel. It organizes the search in two phases. First, a look-ahead solver splits the problem into many sub-problems, called cubes, which are then solved in parallel by incremental CDCL solvers. In this tool paper we present the first fully integrated and automatic distributed cube-and-conquer solver Paracooba targeting cluster and cloud computing. Previous work was limited to multi-core parallelism or relied on manual orchestration of the solving process. Our approach uses one master per problem to initialize the solving process and automatically discovers and releases compute nodes through elastic resource usage. Multiple problems can be solved in parallel on shared compute nodes, controlled by a custom peer-to-peer based load-balancing protocol. Experiments show the scalability of our approach.
For the entire collection see [Zbl 1457.68014].


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.)
Full Text: DOI