Aperture: an Anytime, Complete and Incremental MaxSAT Solver

Abstract

Anytime MaxSAT solving is indispensable in applications that require finding near-optimal solutions within a flexible, user-controlled time budget. Recent years have seen substantial progress in anytime MaxSAT algorithms, including the introduction of SAT-based local search, the development of efficient approximation techniques, and significant advancements in classical local search algorithms. However, all leading anytime solvers—including the winners of the three latest MaxSAT Evaluations (MSEs) in the anytime categories—reuse the code base of a single solver, tt-open-wbo-inc, which, while highly efficient, lacks an in-memory API, is non-incremental and incomplete, and contains substantial dead and legacy code. We introduce Aperture, a new anytime MaxSAT solver written from scratch. Aperture is both incremental and complete; it provides in-memory APIs in both C++ (including IPAMIR compliance) and Python. Algorithmically, Aperture follows a similar high-level approach to tt-open-wbo-inc, but employs a unified flow for both weighted and unweighted MaxSAT. Performance-wise, Aperture is highly competitive. Under the benchmark sets and evaluation conditions of MSE’24, it outscores both the MSE’24 winner SPB-MaxSAT-c and tt-open-wbo-inc in all four anytime categories, and in 8 out of 12 such categories across the three most recent MSEs (2022– 2024). Moreover, Aperture outperforms leading non-anytime MaxSAT solvers on 2 out of the 5 incremental benchmark sets from MSE’22, an evaluation setting in which, unlike for anytime categories, both incrementality and completeness are mandatory.