论文标题
一致性关闭的小证据
Small Proofs from Congruence Closure
论文作者
论文摘要
满足性模型理论（SMT）求解器和平等饱和引擎必须从基于电子段的一致性封闭程序中生成证明证书，以实现验证和冲突条款生成。较小的证明证书加快了这些活动。尽管已知生成最小尺寸的证据的问题已知NP完整，但现有的证明最小化算法的一致性关闭算法会产生不必要的大量证明，并在核心一致性封闭过程中引入渐近间接费用。在本文中，我们引入了O（n^5）时间算法，该算法在新的放松的“证明树大小”度量标准下生成最佳证明，该算法直接限制了证明大小。然后，我们将这种方法进一步放松到实用的O（n \ log（n））贪婪算法，该算法生成没有渐近头顶的少量证明。我们在鸡蛋平等饱和工具包中实施了技术，从而获得了第一个认证的平等饱和引擎。我们表明，与3760个基准的语料库上的最先进的Z3 SMT求解器相比，我们的鸡蛋中的贪婪方法很快产生的证明较小。
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.
