Certifying Top-Down Decision-DNNF Compilers

Certifying Top-Down Decision-DNNF Compilers
复制标题

认证自上而下决策 DNNF 编译器

DOI：
--
复制
发表时间：
2021
期刊：
AAAI Conference on Artificial Intelligence
影响因子：
--
通讯作者：
P. Marquis
P. Marquis
中科院分区：
--
文献类型：
--
作者：
Florent Capelli;Jean;P. Marquis

文献摘要

被引文献

相似文献

验证解决复杂问题的工具的输出，以确保 他们提供的结果的正确性非常重要。 尽管 SAT 求解者普遍存在这种程度的紧急情况 尚未渗透到解决更复杂任务的工具，例如模型 计数或知识汇编。本文的重点是 自上而下的 Decision-DNNF 编译器的通用系列。我们解释这些如何 可以调整编译器以输出可验证的决策-DNNF 电路，主要是由标准Decision-DNNF电路装饰 注释充当证书。我们描述一个多项式时间 用于测试给定 CNF 公式是否等效的检查器 给定的可验证决策-DNNF 电路。最后，利用 用于生成可证明的编译器 d4 的修改版本 我们提出了决策 DNNF 电路和检查器的实现 已进行的实证评估的结果 评估实践中可验证的决策 DNNF 电路有多大， 以及需要多少时间来计算和检查这些电路。
Certifying the output of tools solving complex problems so as to ensure the correctness of the results they provide is of tremendous importance. Despite being widespread for SAT-solvers, this level of exigence has not yet percolated for tools solving more complex tasks, such as model counting or knowledge compilation. In this paper, the focus is laid on a general family of top-down Decision-DNNF compilers. We explain how those compilers can be tweaked so as to output certifiable Decision-DNNF circuits, which are mainly standard Decision-DNNF circuits decorated by annotations serving as certificates. We describe a polynomial-time checker for testing whether a given CNF formula is equivalent or not to a given certifiable Decision-DNNF circuit. Finally, leveraging a modified version of the compiler d4 for generating certifiable Decision-DNNF circuits and an implementation of the checker, we present the results of an empirical evaluation that has been conducted for assessing how large are in practice certifiable Decision-DNNF circuits, and how much time is needed to compute and to check such circuits.