@inproceedings{BergSJ:IJCAI2015,
author = {Jeremias Berg and Paul Saikko and Matti J\"arvisalo},
title = {Improving the Effectiveness of {SAT}-Based Preprocessing for {MaxSAT}},
editor = {Qiang Yang and Michael Wooldridge},
booktitle = {Proceedings of the 24th International Joint Conference on 
              Artificial Intelligence (IJCAI 2015)},
pages = {239--245},
year = {2015},
publisher = {AAAI Press},
}

Abstract:

Solvers for the Maximum satisfiability (MaxSAT) problem
find an increasing number of applications today.  We 
focus on improving  MaxHS---one of the most successful 
recent MaxSAT algorithms---via SAT-based preprocessing.
We show that employing SAT-based preprocessing via the 
so-called labelled CNF (LCNF) framework before calling 
MaxHS can in some cases greatly degrade performance of 
the solver. As a remedy, we propose a lifting of MaxHS 
that works directly on LCNFs,  allowing for a tighter 
integration of SAT-based preprocessing and MaxHS. Our 
empirical results on standard crafted and industrial 
weighted partial MaxSAT Evaluation benchmarks show 
overall improvements over the original MaxHS algorithm
both with and without SAT-based preprocessing.