Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
复制标题
DOI：
10.1613/jair.3196
复制
发表时间：
2011-01-01
影响因子：
5
通讯作者：
Sebastiani, Roberto
中科院分区：
文献类型：
--
作者：
Cimatti, Alessandro;Griggio, Alberto;Sebastiani, Roberto
寻找SAT公式的小不可满足核的问题最近受到了很多关注，主要是因为它在形式验证中的应用。然而，命题逻辑往往没有足够的表达来表示许多有趣的验证问题，这可以更自然地解决在可满足性模理论，SMT的框架。令人惊讶的是，在SMT中找到不可满足的核心的问题在文献中很少受到关注。在本文中，我们提出了一种新的方法来解决这个问题，称为引理提升方法。其主要思想是联合收割机SMT求解器与外部命题核心提取器相结合。SMT求解器产生在搜索期间发现的理论引理，动态地将适量的理论信息提升到布尔级别。核心提取器，然后调用原始SMT问题和理论引理的布尔抽象。这将导致一个不可满足的核心，为原来的SMT问题，一旦剩余的理论引理被删除。这种方法在概念上很有趣，在实践中有几个优点。事实上，它的实现和更新非常简单，并且它可以以即插即用的方式与每个命题核心提取器接口，以便免费受益于已经或将要提供的所有不饱和核心还原技术。我们已经评估了我们的算法与一个非常广泛的实证测试SMT-LIB基准，这证实了这种方法的有效性和潜力。
The problem of finding small unsatisfiable cores for SAT formulas has recently received a lot of interest, mostly for its applications in formal verification. However, propositional logic is often not expressive enough for representing many interesting verification problems, which can be more naturally addressed in the framework of Satisfiability Modulo Theories, SMT. Surprisingly, theproblem of finding unsatisfiable cores in SMT has received very little attention in the literature. In this paper we present a novel approach to this problem, called the Lemma-Lifting approach. The main idea is to combine an SMT solver with an external propositional core extractor. The SMT solver produces the theory lemmas found during the search, dynamically lifting the suitable amount of theory information to the Boolean level. The core extractor is then called on the Boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas are removed. The approach is conceptually interesting, and has several advantages in practice. In fact, it is extremely simple to implement and toupdate, and it can be interfaced with every propositional core extractor in a plug-and-play manner, so as to benefit for free of all unsat-core reduction techniques which have been or will be made available. We have evaluated our algorithm with a very extensive empirical test on SMT-LIB benchmarks, which confirms the validity and potential of this approach.