Modern competitive solvers employ various pre- and inprocessing techniques to efficiently tackle complex problems. This work introduces two pre- and inprocessing techniques to improve solving weighted partial MaxSAT problems: Generalized Boolean Multilevel Optimization (GBMO) and Trimming MaxSAT (TrimMaxSAT).

GBMO refines and extends Boolean Multilevel Optimization (BMO), thereby splitting instances due to their distribution of weights into multiple less complex subproblems, which are solved one after the other to obtain the overall solution.

The second technique, TrimMaxSAT, finds unsatisfiable soft clauses and removes them from the instance. This reduces the complexity of the MaxSAT instance and works especially well in combination with GBMO. The proposed algorithm works incrementally in a binary search fashion, testing the satisfiability of every soft clause. Furthermore, as a by-product, typically an initial weight close to the maximum is found, which is in turn advantageous w.r.t. the size of e.g. the Dynamic Polynomial Watchdog (DPW) encoding.

Experimental results show the effectiveness of both techniques on a large set of benchmarks from a hardware security application and from the 2019 MaxSAT Evaluation. In particular for the hardest of the application benchmarks, the solver Pacose with GBMO and TrimMaxSAT performs best compared to the MaxSAT Evaluation solvers of 2019. For the benchmarks of the 2019 MaxSAT Evaluation, we show that with the proposed techniques the top solver combination solves significantly more instances.