MUP

Mup: a minimal unsatisfiability prover. After establishing the unsatisfiability of a SAT instance encoding a typical design task, there is a practical need to identify its minimal unsatisfiable subsets, which pinpoint the reasons for the infeasibility of the design. Due to the potentially expensive computation, existing tools for the extraction of unsatisfiable subformulas do not guarantee the minimality of the results. This paper describes a practical algorithm that decides the minimal unsatisfiability of any CNF formula through BDD manipulation. This algorithm has a worse-case complexity that is exponential only in the treewidth of the CNF formula. We provide an empirical evaluation of the algorithm, highlighting its efficiency on a set of hard problems as well as its ability to work with existing subformula extraction tools to achieve optimal results.

This software is also peer reviewed by journal TOMS.


References in zbMATH (referenced in 14 articles )

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

  1. Schuppan, Viktor: Extracting unsatisfiable cores for LTL via temporal resolution (2016)
  2. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  3. Gupta, Ashutosh: Improved single pass algorithms for resolution proof reduction (2012)
  4. Cimatti, A.; Griggio, A.; Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories (2011)
  5. Desrosiers, Christian; Galinier, Philippe; Hertz, Alain; Paroz, Sandrine: Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems (2009)
  6. Grégoire, Éric; Mazure, Bertrand; Piette, Cédric: Does this set of clauses overlap with at least one MUS? (2009)
  7. Liffiton, Mark; Mneimneh, Maher; Lynce, In^es; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas (2009)
  8. Gershman, Roman; Koifman, Maya; Strichman, Ofer: An approach for extracting a small unsatisfiable core (2008)
  9. Liffiton, Mark H.; Sakallah, Karem A.: Algorithms for computing minimal unsatisfiable subsets of constraints (2008)
  10. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto: A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories (2007)
  11. Grégoire, Éric; Mazure, Bertrand; Piette, Cédric: Local-search extraction of mUSes (2007)
  12. Dershowitz, Nachum; Hanna, Ziyad; Nadel, Alexander: A scalable algorithm for minimal unsatisfiable core extraction (2006)
  13. Liffiton, Mark H.; Sakallah, Karem A.: On finding all minimally unsatisfiable subformulas (2005)
  14. Mneimneh, Maher; Lynce, In^es; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem: A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas (2005)