Accelerating MUS extraction with recursive model rotation

Minimally Unsatisfiable Subformulas (MUSes) find a wide range of practical applications. A large number of MUS extraction algorithms have been proposed over the last decade, and most of these algorithms are based on iterative calls to a SAT solver. In this paper we introduce a powerful technique for acceleration of MUS extraction algorithms called recursive model rotation - a recursive version of the recently proposed model rotation technique. We demonstrate empirically that recursive model rotation leads to multiple orders of magnitude performance improvements on practical instances, and pushes the performance of our MUS extractor MUSer2 ahead of the currently available MUS extraction tools.