- AAAI构建精确的伪布尔模型计数器
我们提出了第一个准确的伪布尔模型计数器 PBCount,它通过代数决策图的知识编译方法来实现。我们的实证评估表明,PBCount 可以计算 1513 个实例的计数,而当前最先进的方法只能处理 1013 个实例。我们的工作为进一步研究伪布尔公 - MM可增量优化的任意时刻答案集计数
该论文介绍了一种通过假设知识编译来迭代计算答案集的技术,以改进对解空间的估计,同时避免了在计算中的指数级开销。
- 自顶向下计数模理论知识编译
该研究讨论了 #SMT 的编译策略,提出了一种基于穷尽 DPLL (T) 搜索的自上而下的编译器。
- 为 Shap Score 计算打开神经网络分类器
本文研究了如何高效地计算机器学习模型中的 Shap 解释得分,通过将二元神经网络转换为确定性和可分解的布尔电路,并利用知识编译技术,将所得到的电路作为开放框模型来计算 Shap 分数,与将 BNN 作为黑盒模型直接计算 Shap 相比,在性 - MM高效知识编译:超越带权模型计数
本文介绍了用于解决量化扩展逻辑编程中的第二级推理任务的算法框架 Second Level Algebraic Model Counting (2AMC),探讨了使用知识编译技术降低处理效率时的需要考虑变量阶数限制问题,进一步提出并实现了一种 - CCDD: 模型计数和均匀采样的可处理表示
本文提出一种新的表示语言 CCDD,并利用其支持的多项式算法在模型计数和一致采样上显著改进于目前最先进的 Decision-DNNF,SDD 和 OBDD [AND] 编译器,以及在 CNF 上开发模型计数器和一致采样器。
- MM知识编译中的相变行为
研究随机 k-CNF 公式的规模和编译时间行为,以及使用知识编译进行的大小和运行时行为的严格实证研究和分析,类似于 SAT / CSP 社区对相变行为的早期研究,我们鉴定了不同参数方面的有趣行为:子句密度和解密度,并总结我们的经验研究。
- 布尔函数综合的知识编译
研究 Boolean functional synthesis 问题中 CNF 转化为 SynNNF 的算法,并证明 SynNNF 具有多项式时间综合的优势。
- 句子决策图的相对简洁性
本文旨在确定哪些布尔函数可以由小型的 SDDs 表示,同时将多项式大小的布尔函数表示集合与来自 Darwiche 和 Marquis 经典知识编译地图的表示类型进行比较。最主要的结果是通过等效的不明确的非确定性 OBDDs 对 SDDs 进 - SDDs 比 OBDDs 更为简洁
本文介绍了一种名为 sentential decision diagrams (SDDs) 的表达语言,证明了在布尔函数的表示中 SDDs 比 ordered binary decision diagrams (OBDDs) 更简洁,该结论 - 知识编译的新极限及其在精确模型计数中的应用
论文提出了关于大规模自然问题中精确概率推断效率的新极限,尤其是给出了关于知识编译到 SDD 和 DNNF 形式的新下限,并利用 SDD 大小与最佳划分通信复杂度的关系证明了一类大型问题的 SDD 大小的指数下限。
- 团宽和知识编译
本文研究了丛图宽度在布尔函数简洁表示中的作用,并推出了相应结论。该结论表明,丛图宽度对于表示布尔函数并不比树宽更加 “强大”,并且演示了该结论在知识编译中的应用。同时提出了一种可行的算法,能够将丛图宽度小于等于 k 的布尔电路编译成大小为 - 代数模型计数
介绍了代数模型计数(AMC),它是对半环结构加权模型计数(WMC)的推广。研究表明,AMC 泛化了众多领域的很多任务如概率推理,软限制和网络和数据库分析。此外,该研究还从知识编译角度研究了 AMC,并表明所有的 AMC 任务都可以使用 sd - 知识编译地图
本文提供了一种知识编译的角度,分析了不同的编译方法(依据目标编译语言的简洁性与语言在多项式时间内支持的查询和转换的类别),并提供了一张知识编译图使新的编译方法能在已有方法的背景下进行分析。
- 知识编译中的相变:实验研究
本文研究了知识编译中的相变现象,通过对随机 k-SAT 实例进行实验,发现编译结果存在易 - 难 - 易的规律,且大小峰值仅与子句数与变量数比例的固定值有关,大多数编译结果大小随变量数增加呈指数增长,但也存在一种相变现象,该相变由 DFA