Treffer: 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 Painless 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 D-Painless, a new extension of the Painless framework to include the distributed portfolio strategy and clause sharing. Our enhancement aims to broaden Painless's functionality, enabling more effective and comprehensive distributed SAT solving methodologies.