文献学习——Faster Extraction of High-Level Minimal Unsatisfiable Cores

Various verification techniques are based on SAT’s capability to identify a small, or even minimal, unsatisfiable core in case the formula is unsatisfiable, i.e., a small subset of the clauses that are unsatisfiable regardless of the rest of the formula.

译文：各种验证技术都基于SAT的能力，在公式不满足的情况下识别一个小的，甚至最小的，不满足的核心，即，一个小子集的子句是不满足的，不管公式的其他部分。

In most cases it is not the core itself that is being used, rather it is processed further in order to check which clauses from a preknown set of Interesting Constraints (where each constraint is modeled with a conjunction of clauses) participate in the proof. 

译文：在大多数情况下，并不是使用核心本身，而是进一步处理它，以便检查已知的有趣约束集(其中每个约束都用子句连词建模)中的哪些子句参与证明。

The problem of minimizing the participation of interesting constraints was recently coined high-level minimal unsatisfiable core by Nadel [15].译文：最小化有趣约束参与的问题是最近由纳达尔·[15]创造的高级最小不可满足核心。

Two prominent examples of verification techniques that need such small cores are ：

1) abstraction-refinement model-checking techniques, which use the core in order to identify the state variables that will be used for refinement (smaller number of such variables in the core implies that more state variables can be replaced with free inputs in the abstract model)。

2) assumption minimization, where the goal is to minimize the usage of environment assumptions in the proof, because these assumptions have to be proved separately. 译文：2)假设最小化，目标是在证明中尽量减少使用环境假设，因为这些假设必须分别证明。

译文：两个需要这样小核心的验证技术的突出例子是:

    1)抽象-细化模型检查技术;它们使用核心来识别将用于细化的状态变量(核心中此类变量的数量越少，意味着在抽象模型中可以用自由输入替换更多的状态变量)

    2)假设最小化，目标是在证明中尽量减少使用环境假设，因为这些假设必须分别证明。

译文：我们对[15]中给出的最近的解决方案提出了七个改进，根据我们对数百个工业测试用例的实验，这些改进共同导致运行时间总体上减少了55%，结果核心的大小减少了73%。优化的过程在经验上也优于基于假设的最小化技术。