Structure-Guided Cube-and-Conquer for MaxSAT

We present a black-box inprocessor for the partially weighted maximum satisfiability problem, which extends any given MaxSAT solver with inprocessing capabilities without modifying the core solver. Our approach combines the well-established cube-and-conquer technique with classical dynamic programming over a tree decomposition of the formula. While the first technique is limited in the size of the cubes it can handle, the second technique is limited by the treewidth of the input. By combining both paradigms, we cam handle significantly bigger cubes in instances with a treewidth of over a thousand, all without suffering performance losses on unstructured instances. Through an extensive experimental study, we demonstrate the efficiency of our approach in enhancing established implementations of various standard algorithms for MaxSAT. Our results showcase that structure-guided cube-and-conquer can serve as a general black-box inprocessor for MaxSAT, making it a valuable addition to the MaxSAT toolbox.