@inproceedings{BergSJ:ICTAI2015,
author = {Jeremias Berg and Paul Saikko and Matti J\"arvisalo},
title = {Re-using Auxiliary Variables for {MaxSAT} Preprocessing},
booktitle = {Proceedings of the 2015 IEEE 27th International Conference on 
             Tools with Artificial Intelligence (ICTAI 2015)},
pages = {813--820},
year = {2015},
publisher = {IEEE Computer Society}
}

Abstract:

Solvers for the maximum satisfiability (MaxSAT) problem---a well-known 
optimization variant of Boolean satisfiability (SAT)---are finding an 
increasing number of applications. Preprocessing has proven an integral 
part of the SAT-based approach to efficiently solving various types of 
real-world problem instances. It was recently shown that SAT 
preprocessing for MaxSAT becomes more effective by re-using the 
auxiliary variables introduced in the preprocessing phase directly in 
the SAT solver within a core-based hybrid MaxSAT solver. We take this 
idea of re-using auxiliary variables further by identifying them among 
variables already present in the input MaxSAT instance. Such variables 
can be re-used already in the preprocessing step, avoiding the 
introduction of multiple layers of new auxiliary variables in the 
process. Empirical results show that by detecting auxiliary variables in 
the input MaxSAT instances can lead to modest additional runtime 
improvements when applied before preprocessing. Furthermore, we show 
that by re-using auxiliary variables not only within preprocessing but 
also as assumptions within the SAT solver of the MaxHS MaxSAT algorithm 
can alone lead to performance improvements similar to those observed by 
applying SAT-based preprocessing.