MUSer2: an efficient MUS extractor. 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 for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Ivrii, Alexander; Malik, Sharad; Meel, Kuldeep S.; Vardi, Moshe Y.: On computing minimal independent support and its applications to sampling and counting (2016)
- Liffiton, Mark H.; Previti, Alessandro; Malik, Ammar; Marques-Silva, Joao: Fast, flexible MUS enumeration (2016)
- Grégoire, Éric; Lagniez, Jean-Marie; Mazure, Bertrand: On getting rid of the preprocessing minimization step in MUC-finding algorithms (2015)
- Belov, Anton; Marques-Silva, Joao: MUSer2: an efficient MUS extractor (2014)
- Belov, Anton; Manthey, Norbert; Marques-Silva, Joao: Parallel MUS extraction (2013)