HaifaHSmtMuc (HSmtMuc)

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.


HMUC algorithm
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

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