CVC4 中基于 DRAT 的位向量证明
计算机科学中的逻辑
2019-07-04 v2
摘要
许多用于固定大小位向量理论的前沿 SMT（Satisfiability Modulo Theories，可满足性模理论）求解器采用称为位 blasting（bit-blasting）的方法，将给定的公式翻译为布尔可满足性（SAT）问题并委托给 SAT 求解器。因此，在 SMT 求解器中生成位向量证明需要将其 SAT 证明整合进证明基础设施。在本文中，我们描述了三种将现成 SAT 求解器生成的 DRAT 证明整合进 SMT 求解器 CVC4 的证明基础设施的方法，并探讨它们的优缺点。我们使用 cryptominisat 作为其位 blasting 引擎的 SAT 后端实现了所有三种方法，并从证明生成和证明检查方面评估了性能。
引用
@article{arxiv.1907.00087,
title = {DRAT-based Bit-Vector Proofs in CVC4},
author = {Alex Ozdemir and Aina Niemetz and Mathias Preiner and Yoni Zohar and Clark Barrett},
journal= {arXiv preprint arXiv:1907.00087},
year = {2019}
}