扩展SMT求解：非基子句学习
Extending SMT Solving with Non-Ground Clause Learning
浏览论文内容
中文总结 AI 辅助
本文提出一种结合基实例化、CDCL(T)风格规则与非基冲突分析的演算，通过非基子句学习生成更一般的子句，并支持时间回溯，可模拟多种SMT求解方法。
中文摘要 AI 辅助
量词实例化是目前非基SMT求解的主要方法：求解器生成基实例，并通过CDCL(T)风格的推理求解所得的基SMT问题。当发现冲突时，冲突分析仅学习一个基子句，即使该冲突源自非基子句的实例。然而，非基推理可以给出比纯基推理指数级更短的证明。我们提出了一种由基实例化、CDCL(T)风格规则和非基冲突分析组成的演算。求解器在基实例上进行推理，但冲突分析的消解步骤在其原始非基子句上执行。这产生的学习子句通常比基冲突更一般。通过合适的策略，学习到的子句甚至是非冗余的。我们还展示了如何将时间回溯纳入SMT求解。我们的演算为CDCL(T)风格的SMT求解、一系列基于实例化的过程以及非基子句学习提供了一个通用框架，并证明了它可以模拟CDCL、SCL(FOL)、SCL(T)甚至Resolution。
英文摘要
Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style reasoning. When a conflict is found, conflict analysis learns only a ground clause, even though the conflict comes from instances of non-ground clauses. Yet non-ground reasoning can give exponentially shorter proofs than purely ground reasoning. We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. The solver reasons on ground instances, but the resolution steps of conflict analysis are performed on their original non-ground clauses. This produces learned clauses that are typically more general than the ground conflict. With a suitable strategy, the learned clauses are even non-redundant. We also show how chronological backtracking can be included in SMT solving. Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning, and we prove that it simulates CDCL, SCL(FOL), SCL(T), and even Resolution.
发表机构
- Max Planck Institute for Informatics（马克斯·普朗克信息学研究所）
- Graduate School of Computer Science, Saarland Informatics Campus（萨尔兰信息学园区计算机科学研究生院）
机构由 AI 辅助整理，请以论文原文为准。
