HaifaMUC (HMUC) is a minimal unsatisfiable core (MUC) extractor, based on Minisat 2.2.
- Download Version 1.3 (the SAT’15 version) [Linux x64 executable]
- Download Version 1.2 (the FMCAD’13 version)
- Download Version 1.0 (the 2011 competition version)
Related publications:
- Alexander Ivrii, Vadim Ryvchin, Ofer Strichman
Mining Backbone Literals in Incremental SAT – a new kind of incremental data
Proc. of the 18th International conference on theory and applications of satisfiability testing (SAT’15), pages 88-103. Detailed experimental results: SAT’02-beta benchmarks, and SAT’11/MUS benchmarks
LPF is invoked with -pf-mode=3, and LPFi with -pf-mode=4. - Alexander Nadel, Vadim Ryvchin, Ofer Strichman
Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores
Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 9 (2014), pages 27-51. - Alexander Nadel, Vadim Ryvchin, Ofer Strichman
Efficient MUS extraction with Resolution
Proc. of the 13th conference on Formal Methods in Computer Aided Design (FMCAD’13).