D-Painless: A Framework for Distributed Portfolio SAT Solving

Abstract

Abstract 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 "Image missing" 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 "Image missing" , a new extension of the "Image missing" framework to include the distributed portfolio strategy and clause sharing. Our enhancement aims to broaden "Image missing" ’s functionality, enabling more effective and comprehensive distributed SAT solving methodologies.