带显式依赖的综合
计算机科学中的逻辑
2023-01-26 v1 人工智能
摘要
量化布尔公式（QBF）以量化 扩展命题逻辑。在 QBF 中，存在量化变量允许依赖于其辖域内所有全称量化变量。依赖量化布尔公式（DQBF）限制存在量化变量的依赖关系。在 DQBF 中，存在量化变量对称为 Henkin 依赖的全称量化变量子集具有显式依赖。给定输入与输出集合间的布尔规约，Henkin 综合问题是综合每个输出变量作为其 Henkin 依赖的函数，以满足规约。Henkin 综合具有广泛应用，包括部分电路验证、控制器综合与电路可实现性。本工作提出一种称为 Manthan3 的用于 Henkin 综合的数据驱动方法。在对来自过往 DQBF 求解竞赛的超过 563 个实例的广泛评估中，我们证明 Manthan3 与最先进工具具有竞争力。此外，Manthan3 能为 26 个基准综合 Henkin 函数，而最先进技术均无法综合。
引用
@article{arxiv.2301.10556,
title = {Synthesis with Explicit Dependencies},
author = {Priyanka Golia and Subhajit Roy and Kuldeep S. Meel},
journal= {arXiv preprint arXiv:2301.10556},
year = {2023}
}
备注
To be published in Design, Automation and Test in Europe Conference (DATE), 2023