D-Painless: A Framework for Distributed Portfolio SAT Solving
摘要
In the evolving landscape of SAT solving, leveraging parallel computation has become increasingly significant. The portfolio strategy, combined with clause sharing, has emerged as the leading approach for both local and distributed parallelization on CPUs. Frameworks such as Mallob exemplify the effectiveness of this strategy by providing a straightforward method to deploy portfolio parallel solvers across various computing environments. Similarly, the framework specializes in local parallelization, offering diverse strategies for task sharing and parallel execution. This enables the adoption of complex hybrid local parallelization techniques, including portfolio, divide-and-conquer, and cube-and-conquer methods. This paper presents , a new extension of the framework to include the distributed portfolio strategy and clause sharing. Our enhancement aims to broaden ’s functionality, enabling more effective and comprehensive distributed SAT solving methodologies.