Distributed Incremental SAT Solving with Mallob: Report and Case Study with Hierarchical Planning
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915303615627264 |
|---|---|
| author | Schreiber, Dominik |
| author_facet | Schreiber, Dominik |
| contents | This report describes an extension of the distributed job scheduling and SAT solving platform Mallob by incremental SAT solving, embedded in a case study on SAT-based hierarchical planning. We introduce a low-latency interface for incremental jobs and specifically for IPASIR-style incremental SAT solving to Mallob. This also allows to process many independent planning instances in parallel via Mallob's scheduling capabilities. In an experiment where 587 planning inputs are resolved in parallel on 2348 cores, we observe significant speedups for several planning domains where SAT solving constitutes a major part of the planner's running time. These findings indicate that our approach to distributed incremental SAT solving may be useful for a wide range of SAT applications. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_18836 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Distributed Incremental SAT Solving with Mallob: Report and Case Study with Hierarchical Planning Schreiber, Dominik Distributed, Parallel, and Cluster Computing Logic in Computer Science This report describes an extension of the distributed job scheduling and SAT solving platform Mallob by incremental SAT solving, embedded in a case study on SAT-based hierarchical planning. We introduce a low-latency interface for incremental jobs and specifically for IPASIR-style incremental SAT solving to Mallob. This also allows to process many independent planning instances in parallel via Mallob's scheduling capabilities. In an experiment where 587 planning inputs are resolved in parallel on 2348 cores, we observe significant speedups for several planning domains where SAT solving constitutes a major part of the planner's running time. These findings indicate that our approach to distributed incremental SAT solving may be useful for a wide range of SAT applications. |
| title | Distributed Incremental SAT Solving with Mallob: Report and Case Study with Hierarchical Planning |
| topic | Distributed, Parallel, and Cluster Computing Logic in Computer Science |
| url | https://arxiv.org/abs/2505.18836 |