同余闭包的小证明
Small Proofs from Congruence Closure
摘要：
可满足性模理论（SMT）求解器和等式饱和引擎必须从基于e图的同余闭包过程生成证明证书，以实现验证和冲突子句生成。较小的证明证书加快了这些活动。虽然生成最小尺寸的证明的问题是NP完全的，现有的证明最小化算法的同余闭包生成不必要的大证明，并引入渐近开销的核心同余闭包过程。在本文中，我们引入了一个O（n^5）时间算法，该算法在一个新的放松的“证明树大小”度量下生成最佳证明，该度量直接限制了证明大小。然后，我们放松这种方法进一步到一个实用的O（n \log（n））贪心算法，产生小的证明，没有渐近开销。我们在egg equality saturation toolkit中实现了我们的技术，产生了第一个验证equality saturation引擎。我们表明，我们的贪婪的方法在鸡蛋快速生成大大小于国家的最先进的Z3 SMT求解器上的3760基准语料库的证明。
英文摘要：
Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification and conflict clause generation. Smaller proof certificates speed up these activities. Though the problem of generating proofs of minimal size is known to be NP-complete, existing proof minimization algorithms for congruence closure generate unnecessarily large proofs and introduce asymptotic overhead over the core congruence closure procedure. In this paper, we introduce an O(n^5) time algorithm which generates optimal proofs under a new relaxed "proof tree size" metric that directly bounds proof size. We then relax this approach further to a practical O(n \log(n)) greedy algorithm which generates small proofs with no asymptotic overhead. We implemented our techniques in the egg equality saturation toolkit, yielding the first certifying equality saturation engine. We show that our greedy approach in egg quickly generates substantially smaller proofs than the state-of-the-art Z3 SMT solver on a corpus of 3760 benchmarks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
