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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

D-Painless: A Framework for Distributed Portfolio SAT Solving

  • Mazigh Saoudi,
  • Souheib Baarir,
  • Julien Sopena,
  • Thibault Lejemble

摘要

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.