Distributed cube and conquer with Paracooba. 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.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Ansótegui, Carlos; Ojeda, Jesús; Pacheco, Antonio; Pon, Josep; Salvia, Josep M.; Torres, Eduard: OptiLog: a framework for SAT-based systems (2021)
- Bjørner, Nikolaj; Levatich, Maxwell; Lopes, Nuno P.; Rybalchenko, Andrey; Vuppalapati, Chandrasekar: Supercharging plant configurations using Z3 (2021)
- Cai, Shaowei; Zhang, Xindi: Deep cooperation of CDCL and local search for SAT (2021)
- Fleury, Mathias; Biere, Armin: Efficient all-UIP learned clause minimization (2021)
- Froleyks, Nils; Heule, Marijn; Iser, Markus; Järvisalo, Matti; Suda, Martin: SAT competition 2020 (2021)
- Manthey, Norbert: The \textscMergeSatsolver (2021)
- Reichl, Franz-Xaver; Slivovsky, Friedrich; Szeider, Stefan: Certified DQBF solving by definition extraction (2021)
- Schreiber, Dominik; Sanders, Peter: Scalable SAT solving in the cloud (2021)
- Trimoska, Monika; Dequen, Gilles; Ionica, Sorina: Logical cryptanalysis with WDSat (2021)
- Heisinger, Maximilian; Fleury, Mathias; Biere, Armin: Distributed cube and conquer with Paracooba (2020)