Minimal unsatisfiable core extraction for SMT.

Finding a minimal (i.e., irreducible) unsatisfiable core (MUC), and high-level minimal unsatisfiable core (also known as group MUC, or GMUC), are well-studied problems in the domain of propositional satisfiability. In contrast, in the domain of SMT, no solver in the public domain produces a minimal or group-minimal core. Several SMT solvers, like Z3, produce a core but do not attempt to minimize it. The SMT solver MathSat has an option to try to make the core smaller, but does not guarantee minimality. In this article we present a method and tool, HSmtMuc, for finding MUC and GMUC for SMT solvers. The method is based on the well-known deletion-based MUC extraction that is used in most propositional MUC extractors, together with several new optimizations such as theory-rotation, and an adaptive activation strategy based on measurements, during execution, of the time consumed by various components, combined with exponential smoothing. We implemented HSmtMuc on top of Z3 and MathSat, and evaluated its performance with hundreds of SMT-LIB benchmarks.