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.

References in zbMATH (referenced in 13 articles , 1 standard article )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Bjørner, Nikolaj; Levatich, Maxwell; Lopes, Nuno P.; Rybalchenko, Andrey; Vuppalapati, Chandrasekar: Supercharging plant configurations using Z3 (2021)
  2. Lagniez, Jean-Marie; Lonca, Emmanuel; Marquis, Pierre: Definability for model counting (2020)
  3. Bendík, Jaroslav; Černá, Ivana: Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets (2018)
  4. Brandt, Felix; Geist, Christian; Peters, Dominik: Optimal bounds for the no-show paradox via SAT solving (2017)
  5. Bendík, Jaroslav; Beneš, Nikola; Barnat, Jiří; Černá, Ivana: Finding boundary elements in ordered sets with application to safety and requirements analysis (2016)
  6. Ivrii, Alexander; Malik, Sharad; Meel, Kuldeep S.; Vardi, Moshe Y.: On computing minimal independent support and its applications to sampling and counting (2016)
  7. Liffiton, Mark H.; Previti, Alessandro; Malik, Ammar; Marques-Silva, Joao: Fast, flexible MUS enumeration (2016)
  8. Balabanov, Valeriy; Ivrii, Alexander: Speeding up MUS extraction with preprocessing and chunking (2015)
  9. Grégoire, Éric; Lagniez, Jean-Marie; Mazure, Bertrand: On getting rid of the preprocessing minimization step in MUC-finding algorithms (2015)
  10. Ivrii, Alexander; Ryvchin, Vadim; Strichman, Ofer: Mining backbone literals in incremental SAT. A new kind of incremental data (2015)
  11. Zielke, Christian; Kaufmann, Michael: A new approach to partial MUS enumeration (2015)
  12. Belov, Anton; Marques-Silva, Joao: MUSer2: an efficient MUS extractor (2014)
  13. Belov, Anton; Manthey, Norbert; Marques-Silva, Joao: Parallel MUS extraction (2013)