Understanding, improving and parallelizing MUS finding using model rotation

Recently a new technique for improving algorithms for extracting Minimal Unsatisfiable Subsets (MUSes) from unsatisfiable CNF formulas called "model rotation" was introduced [Marques-Silva et. al. SAT2011]. The technique aims to reduce the number of times a MUS finding algorithm needs to call a SAT solver. Although no guarantees for this reduction are provided the technique has been shown to be very effective in many cases. In fact, such model rotation algorithms are now arguably the state-of-the-art in MUS finding. This work analyses the model rotation technique in detail and provides theoretical insights that help to understand its performance. These new insights on the operation of model rotation lead to several modifications and extensions that are empirically evaluated. Moreover, it is demonstrated how such MUS extracting algorithms can be effectively parallelized using existing techniques for parallel incremental SAT solving.