Speeding up MUS extraction with preprocessing and chunking

Abstract

In this paper we present several improvements to extraction of a minimal unsatisfiable subformula (MUS) of a Boolean formula. As our first contribution, we describe model rotation on preprocessed formulas and show that preprocessing significantly improves model rotation. We find very convenient to adopt the framework of labeled CNF formulas and we present our algorithms in this more general framework. We use the assumption-based approach for computing MUSes due to its simplicity and the ability to use any SAT-solver as the back-end. However, this comes with a price: it is well-known that the assumption-based approach performs significantly worse than the resolution-based approach. This leads to our second contribution, we show how to bridge the gap between the two approaches using “chunking”. An extensive experimental evaluation shows that our method significantly outperforms state-of-the-art solutions in the context of group MUS extraction.