AMUSE: a minimally-unsatisfiable subformula extractor. This paper describes a new algorithm for extracting unsatisfiable subformulas from a given unsatisfiable CNF formula. Such unsatisfiable ”cores” can be very helpful in diagnosing the causes of infeasibility in large systems. Our algorithm is unique in that it adapts the ”learning process” of a modern SAT solver to identify unsatisfiable subformulas rather than search for satisfying assignments. Compared to existing approaches, this method can be viewed as a bottom-up core extraction procedure which can be very competitive when the core sizes are much smaller than the original formula size. Repeated runs of the algorithm with different branching orders yield different cores. We present experimental results on a suite of large automotive benchmarks showing the performance of the algorithm and highlighting its ability to locate not just one but several cores.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 24 articles )

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

1 2 next

  1. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)
  2. Kalechstain, Jonathan; Ryvchin, Vadim; Dershowitz, Nachum: Hints revealed (2015)
  3. McAreavey, Kevin; Liu, Weiru; Miller, Paul: Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases (2014)
  4. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  5. Audemard, Gilles; Lagniez, Jean-Marie; Simon, Laurent: Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction (2013)
  6. Dellert, Johannes; Zielke, Christian; Kaufmann, Michael: Musticca: MUS extraction with interactive choice of candidates (2013) ioport
  7. Lagniez, Jean-Marie; Biere, Armin: Factoring out assumptions to speed up MUS extraction (2013)
  8. Gupta, Ashutosh: Improved single pass algorithms for resolution proof reduction (2012)
  9. Cimatti, A.; Griggio, A.; Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories (2011)
  10. Marques-Silva, Joao; Lynce, Ines: On improving MUS extraction algorithms (2011)
  11. Ryvchin, Vadim; Strichman, Ofer: Faster extraction of high-level minimal unsatisfiable cores (2011)
  12. Desrosiers, Christian; Galinier, Philippe; Hertz, Alain; Paroz, Sandrine: Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems (2009)
  13. Grégoire, Éric; Mazure, Bertrand; Piette, Cédric: Using local search to find MSSes and MUSes (2009)
  14. Liffiton, Mark; Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas (2009)
  15. Piette, Cédric; Hamadi, Youssef; Saïs, Lakhdar: Efficient combination of decision procedures for MUS computation (2009)
  16. Gershman, Roman; Koifman, Maya; Strichman, Ofer: An approach for extracting a small unsatisfiable core (2008)
  17. Hauck, Scott; DeHon, Andre: Reconfigurable computing. The theory and practice of FPGA-based computation. (2008)
  18. Liffiton, Mark H.; Sakallah, Karem A.: Algorithms for computing minimal unsatisfiable subsets of constraints (2008)
  19. Liffiton, Mark; Sakallah, Karem: Searching for autarkies to trim unsatisfiable clause sets (2008)
  20. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto: A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories (2007)

1 2 next