From Scalable SAT to MaxSAT: Massively Parallel Solution Improving Search

Abstract

Maximum Satisfiability (MaxSAT) is an essential framework for combinatorial optimization at the core of automated reasoning. However, to date, no notable parallelizations with convincing scaling behaviour exist. We suggest to exploit and transfer recent advances in massively parallel SAT solving to perform scalable solution improving search (SIS) for MaxSAT solving. Building upon the distributed job scheduling and SAT solving platform Mallob, we present the first MaxSAT solver that scales to hundreds of cores through a careful combination of parallel and distributed incremental SAT solving, task parallelism and flexible load balancing, and clause sharing within and across SAT solving tasks. Experiments on up to 768 cores (16 nodes) show that our approach clearly outscales state-of-the-art SIS-based MaxSAT solvers, marking a new baseline for parallel MaxSAT solving.