@inproceedings{BergJ:CP2016,
author = {Jeremias Berg and Matti J\"arvisalo},
title = {Impact of {SAT}-Based Preprocessing on Core-Guided {MaxSAT} Solving},
editor = {Michel Rueher},
pages = {66--85},
year = {2016},
booktitle = {Proceedings of the 22nd International Conference on 
	  Principles and Practice of Constraint Programming (CP 2016)},
series = {Lecture Notes in Computer Science},
volume = {9892},
publisher = {Springer},
}

Abstract:

We present a formal analysis of the impact of Boolean satisfiability (SAT) 
based preprocessing techniques on core-guided solvers for the constraint 
optimization paradigm of maximum satisfiability (MaxSAT). We analyze the 
behavior of two solver abstractions of the core-guided approaches. We show that 
SAT-based preprocessing has no effect on the best-case number of iterations 
required by the solvers. This implies that, with respect to best-case 
performance, the potential benefits of applying SAT-based preprocessing in 
conjunction with core-guided MaxSAT solvers are in principle solely a result of 
speeding up the individual SAT solver calls made during MaxSAT search. We also 
show that, in contrast to best-case performance, SAT-based preprocessing can 
improve the worst-case performance of core-guided approaches to MaxSAT.