Techniques inspired by local search for incomplete MaxSAT and the linear algorithm: varying resolution and solution-guided search

We present a MaxSAT algorithm designed to find high-quality solutions when faced with a tight time budget, e.g. five minutes. The motivation stems from the fact that, for many practical applications, time resources are limited and thus a ‘good solution’ suffices. We identify three weaknesses of the linear MaxSAT algorithm that prevent it from effectively computing low-violation solutions early in the search and develop a novel approach inspired by local search to address these issues. Our varying resolution method initially considers a rough view of the soft clauses (low resolution) and with time refines and adds the remaining constraints until the original problem is solved (high resolution). In addition, we combine the technique with solution-guided search. We experimentally evaluate our approach on test bed benchmarks from the MaxSAT Evaluation 2018 and show that improvements can be achieved over the baseline linear MaxSAT algorithm.