MaxSAT Fuzzing and Delta Debugging

Abstract

This article presents the first systematic study to evaluate a suite of automated fuzzing techniques for Maximum Satisfiability (MaxSAT) solvers. It combines large-scale stress testing with a novel MaxSAT-specific delta debugging method to assess and improve solver robustness. A parallel framework orchestrates the generation of millions of structured MaxSAT instances. It efficiently isolates failure-inducing input and distills failing cases into minimal counterexamples for precise failure localization. Over a 100-hour fuzzing effort, this approach revealed previously unknown failures in almost all 43 solvers from recent MaxSAT competitions and in three certificate-producing solvers. Failures ranged from crashes and incorrect optimality bounds to severe performance slowdowns. Notably, a critical soundness error was identified in one certified solver. The resulting corpus of minimal counterexamples was published as a public regression suite. This suite was adopted as a mandatory check in the 2024 MaxSAT Evaluation, helping cut average solver failure rates by more than half. The MaxSAT community quickly embraced these resources: some solver development teams have already integrated our fuzzer into their workflows. The complete tool chain and benchmark corpus are available at Zenodo (Paxian 2025a). Our study demonstrates that systematic fuzz testing coupled with targeted debugging can significantly raise the reliability standards of MaxSAT solvers and provide valuable resources for future solver development.