Maximilian Heisinger, Mathias Fleury, Armin Biere,
"Distributed Cube and Conquer with Paracooba"
: Proc. 23rd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'20), Serie Lecture Notes in Computer Science (LNCS), Vol. 12178, Springer, Seite(n) 114-122, 7-2020
Distributed Cube and Conquer with Paracooba
Sprache des Titels:
Proc. 23rd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'20)
Cube and conquer is currently the most effective approach tosolve hard combinatorial problems in parallel. It organizes the search intwo phases. First, a look-ahead solver splits the problem into many sub-problems, called cubes, which are then solved in parallel by incrementalCDCL solvers. In this tool paper we present the first fully integratedand automatic distributed cube-and-conquer solver Paracooba targetingcluster and cloud computing. Previous work was limited to multi-coreparallelism or relied on manual orchestration of the solving process. Ourapproach uses one master per problem to initialize the solving processand automatically discovers and releases compute nodes through elasticresource usage. Multiple problems can be solved in parallel on sharedcompute nodes, controlled by a custom peer-to-peer based load-balancingprotocol. Experiments show the scalability of our approach.