TT-Open-WBO-Inc: An Efficient Anytime MaxSAT Solver

We present our anytime MaxSAT solver TT-Open-WBO-Inc, focusing on its evolution since the initial version that won both of the weighted incomplete tracks of MaxSAT Evaluation 2019 (MSE19). The solver’s MSE20 version claimed victory in these tracks at MSE20 and secured second place in both unweighted incomplete tracks. The major innovation in the MSE20 version was the integration of SAT-based local search. The contributions of this paper include: (1) Introducing a previously unpublished variant of the SAT-based local search algorithm Polosat, Polosat-OBV, applied by default already in the MSE20 version, and showing its superiority for weighted solving; (2) Describing and analyzing TT-Open-WBO-Inc’s unweighted component, not studied in previous work; (3) Demonstrating that integrating the local search algorithm SATLike into TT-Open-WBO-Inc as a preprocessor enables it to outperform the winners of MSE20 in all four incomplete tracks.