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

TL;DR

Problem: SAT-based hierarchical planning incurs heavy SAT solving across many incremental calls; Approach: extend Mallob with a low-latency, revision-based incremental job interface and an IPASIR-like bridge, using CaDiCaL/Lingeling with clause sharing; Contributions: a scalable architecture and an empirical evaluation on 587 tasks showing a total speedup of $2.63$ and a median speedup of $1.018$ across diverse planning domains, with five domains achieving median speedup $\\ge 2$; Significance: demonstrates Mallob as a viable distributed backend for incremental SAT solving and points to broader applications such as EDA, model checking, and multi-agent path finding.

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.

Figures (6)

• Figure 1: Analysis of Lilotane on IPC 2020 instances (based on data from ref. schreiber2021lilotane). Left: Ratio of time spent on SAT solving for solved instances. Right: CDF for the duration of individual SAT calls on solved instances (note the offset of the $y$ axis). Both $x$ axes are scaled logarithmically.
• Figure 2: Incremental SAT application interface. Left: conventional IPASIR interface with direct linkage of the application code to SAT solver code. Right: our approach. The application is linked with bridge code, which communicates with a running instance of Mallob via the local machine's file system and via inter-process communication.
• Figure 3: Selected (log-log) running times of Lilotane vs. Mallotane, showing five domains with median speedup $\geq 2$ (blue), three domains where no instance was sped up (red), and five domains with notable outliers (orange).
• Figure 4: Speedups of Mallotane (log. scale) relative to the ratio of time sequential Lilotane spent on SAT calls, with $y=1$ highlighted by a black line.
• Figure 5: Distribution over the duration of individual SAT solving calls for sequential Lilotane (L) and for Mallotane (M), separated into SAT and UNSAT results, for commonly solved instances only. The $y$ axes are offset to allow for discerning relevant differences. Since almost all UNSAT calls are very short, we added a separate plot only showing calls which take less than 0.6 s.