MUSer2: An Efficient MUS Extractor

Anton Belov, Joao Marques-Silva


Algorithms for extraction of Minimally Unsatisfiable Subformulas (MUSes) of CNF formulas find a wide range of practical applications, including product configuration, knowledge-based validation, hardware and software design and verification. This paper describes the MUS extractor MUSer2. MUSer2 implements a wide range of MUS extraction algorithms, integrates a number of key optimization techniques, and represents the current state-of-the-art in MUS extraction.


Minimal unsatisfiability, MUS extraction, SAT applications

Full Text:



  • There are currently no refbacks.