Distributed Incremental SAT Solving with Mallob: Report and Case Study with Hierarchical Planning

TL;DR

This paper extends the Mallob platform with incremental SAT solving capabilities, enabling efficient parallel processing of multiple planning problems and demonstrating significant speedups in large-scale experiments.

Contribution

It introduces a low-latency interface for incremental SAT solving in Mallob and applies it to hierarchical planning, showcasing its scalability and efficiency.

Findings

Significant speedups in SAT-based planning tasks

Effective parallel processing of multiple instances

Demonstrated scalability on 2348 cores

Abstract

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.