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 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Bendík, Jaroslav; Černá, Ivana: Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets (2018)
- Brandt, Felix; Geist, Christian; Peters, Dominik: Optimal bounds for the no-show paradox via SAT solving (2017)
- Bendík, Jaroslav; Beneš, Nikola; Barnat, Jiří; Černá, Ivana: Finding boundary elements in ordered sets with application to safety and requirements analysis (2016)
- 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)
- Balabanov, Valeriy; Ivrii, Alexander: Speeding up MUS extraction with preprocessing and chunking (2015)
- Grégoire, Éric; Lagniez, Jean-Marie; Mazure, Bertrand: On getting rid of the preprocessing minimization step in MUC-finding algorithms (2015)
- Ivrii, Alexander; Ryvchin, Vadim; Strichman, Ofer: Mining backbone literals in incremental SAT. A new kind of incremental data (2015)
- Zielke, Christian; Kaufmann, Michael: A new approach to partial MUS enumeration (2015)
- Belov, Anton; Marques-Silva, Joao: MUSer2: an efficient MUS extractor (2014)
- Belov, Anton; Manthey, Norbert; Marques-Silva, Joao: Parallel MUS extraction (2013)