MUSer2: An Efficient MUS Extractor

Anton Belov, Joao Marques-Silva

Abstract


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.

Keywords


Minimal unsatisfiability, MUS extraction, SAT applications

Full Text:

PDF

Refbacks

  • There are currently no refbacks.