文献学习——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.

译文：求最小(即不可约)不可满足核(MUC)和高级最小不可满足核(也称为群MUC或GMUC)是命题可满足领域中研究得比较充分的问题。

In contrast, in the domain of SMT, no solver in the public domain produces a minimal or group-minimal core.

译文：相反，在SMT领域中，公共领域中的求解器不会产生最小或组最小核心。

Several SMT solvers, like Z3, produce a core but do not attempt to minimize it. 译文：一些SMT求解器(如Z3)会产生一个核心，但不会试图将其最小化。

The SMT solver MATHSAT has an option to try to make the core smaller, but does not guarantee minimality. 译文：SMT求解器MATHSAT有一个选项可以尝试使核心更小，但不能保证最小化。

In this article we present a method and tool, HSMTMUC, for finding MUC and GMUC for SMT solvers. 译文：在本文中，我们提出了一种方法和工具，HSMTMUC，为SMT求解器寻找MUC和GMUC。

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. 译文：该方法基于众所周知的基于删除的MUC提取，这是在大多数命题MUC提取器中使用的，加上一些新的优化，如理论旋转，和自适应激活策略，基于测量，在执行过程中，各种组件所消耗的时间，结合指数平滑。

We implemented HSMT-MUC on top of Z3 and MATHSAT, and evaluated its performance with hundreds of SMT-LIB benchmarks. 译文：我们在Z3和MATHSAT上实现了HSMT-MUC，并使用数百个SMT-LIB基准测试来评估其性能。