HaifaSmtMuc (HSmtMUC) is a minimal unsatisfiable core extractor for SMT formulas.
HSmtMuc is a tool for extracting a minimal unsatisfiable core of Satisfiability Modulo Theories (SMT) formulas. It is implemented on top of Microsoft’s Z3 SMT solver.
Background
Given an unsatisfiable formula in conjunctive normal form (CNF), an unsatisfiable core (UC) is any subset of these clauses that is still unsatisfiable. An unsatisfiable core is called minimal if it is irreducible, i.e., no single clause can be removed without making the formula satisfiable. A minimal core is also a minimum core if its size is the smallest possible for an unsatisfiable core. HSmtMuc finds minimal cores, which are not necessarily minimum.
Useful Links
Source code + executables (for windows): GitHub Repository
Benchmarks
Results
Contact Info
Ofer Strichman: website email: ofers@ie.technion.ac.il
Ofer Guthmann emai: ofer.guthmann@cs.technion.ac.il
Anna Trostanetski email: annat@cs.technion.ac.il