@inproceedings{BelovJMS:TACAS2013,
 author = {Anton Belov and Matti J\"arvisalo and Joao Marques-Silva},
 title  = {Formula Preprocessing in {MUS} Extraction},
 editor = {Nir Piterman and Scott Smolka},
 booktitle = {Proceedings of the 19th International Conference on 
Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2013)},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 volume = {7795},
 pages  = {110--125},
 year   = {2013},
}

Abstract:

Efficient algorithms for extracting minimally unsatisfiable subformulas 
(MUSes) of Boolean formulas find a wide range of applications in the analysis 
of systems, e.g., hardware and software bounded model checking. In this paper 
we study the applicability of preprocessing techniques for Boolean 
satisfiability (SAT) in the context of MUS extraction. Preprocessing has 
proven to be extremely important in enabling more efficient SAT solving. Hence 
the study of the applicability and the effectiveness of preprocessing in MUS 
extraction is highly relevant. Considering the extraction of both standard and 
group MUSes, we focus on a number of SAT preprocessing techniques, and 
formally prove to what extent the techniques can be directly applied in the 
context of MUS extraction. Furthermore, we develop a generic theoretical 
framework that captures MUS extraction problems, and enables formalizing 
conditions for correctness-preserving applications of preprocessing techniques 
that are not applicable directly. We experimentally evaluate the effect of 
preprocessing in the context of group MUS extraction.