AAAIJul, 2019

基于代数决策图的加权模型计数

PDF
TL;DR使用动态规划算法和代数决策图作为主要数据结构来计算布尔公式的精确文字加权模型计数，并将该方法实现在 ADDMC 中，通过在 1914 个标准模型计数基准测试中的比较，展示 ADDMC 在加权模型计数上显著优于现有最佳的求解器。
model countingconjunction normal formdynamic programmingalgebraic decision diagramsexact weighted model counters
发现论文，激发创造
  • PBCounter: 伪布尔公式上的加权模型计数

    基于动态规划算法框架 ADD，我们提出了一种加权伪布尔计数工具 PBCounter 来对伪布尔公式进行加权模型计数，并且通过与基于 CNF 公式的模型计数工具进行实验比较，结果显示 PBCounter 在 CNF 公式上具有更好的性能。

    Dec, 2023

  • DPMC：基于项目连接树的动态规划加权模型计数

    提出了一种动态编程框架来计算 CNF 中公式的精确带权模型计数，其中包括 project-join 树的计划阶段和执行阶段，以及基于约束满足启发式与树分解工具的规划阶段，以及与张量比较的不同数据结构的执行阶段。与 cachet、c2d、d4 和 miniC2D 等最先进的精确带权模型计数器相比，该框架是有竞争力的。

    Aug, 2020

  • 代数模型计数

    介绍了代数模型计数（AMC），它是对半环结构加权模型计数（WMC）的推广。研究表明，AMC 泛化了众多领域的很多任务如概率推理，软限制和网络和数据库分析。此外，该研究还从知识编译角度研究了 AMC，并表明所有的 AMC 任务都可以使用 sd-DNNF 电路来评估。

    Nov, 2012

  • 学习推理：利用神经网络实现近似 DNF 计数

    本文提出了一种基于神经网络模型的加权 #DNF 模型计数方法，结合了近似模型计数和深度学习，可以在线性时间内准确估算模型数目，并在大规模 #DNF 实例中表现良好。

    Apr, 2019

  • 带有有向无环图公理的加权一阶模型计数

    该论文研究的是加权一阶模型计数问题 (WFOMC)，主要关注于能够在多项式时间内进行 WFOMC 的逻辑片段，其中包括经过拓展的两变量一阶逻辑碎片及其衍生的包含计数量词的逻辑碎片，通过在关系上添加定向无环图 (DAG) 公理，这篇论文对子领域进行了扩展。

    Feb, 2023

  • Davis-Putnam 程序在计数模型中的应用

    通过使用 Davis-Putnam 算法，提出了一种算法 CDP，用于计算 CNF 或 DNF 公式的模型的准确数量，该算法的平均运行时间是 O (nm^d)，在大量的 CNF formulas 实验中的实际表现已经被估计。

    Jun, 2011

  • 高效知识编译：超越带权模型计数

    本文介绍了用于解决量化扩展逻辑编程中的第二级推理任务的算法框架 Second Level Algebraic Model Counting (2AMC)，探讨了使用知识编译技术降低处理效率时的需要考虑变量阶数限制问题，进一步提出并实现了一种静态生成约束的策略，并在多个任务和基准测试上评估了有效性。

    May, 2022

  • 正式验证的近似模型计数

    我们提出了第一个近似模型计数的认证框架，并且证明了其输出近似值的质量保证。

    Jun, 2024

  • SAT 问题的分布感知抽样和加权模型计数

    本文介绍了一种新的方法，使用黑箱预言机，通过 NP-Oracle 实际求解带权重赋值的模型计数问题和分布感知的满足分配的抽样问题，从而在中等规模的问题上获得了强大的理论保证。

    Apr, 2014

  • 带基数约束和计数量词的 FO2 加权模型计数：一个封闭式公式

    本文介绍了一种新的 lifted interpretations 工具，用于重构 Beame et al. 提出的多项式时间 FOMC 的闭合式公式，并将其扩展以涵盖基数约束、存在量词和计数量词（C2），同时仍然保持 domain-liftability。最后，我们展示了所获得的闭合形式促进了一种权重函数家族的自然定义，严格大于对称权重函数。

    Oct, 2021