该研究论文探讨了如何通过增加短的随机奇偶约束来计算公式满足的真实赋值(模型),实现 NP 问题的计数,尤其是当需要添加多个约束时,随机奇偶约束的集合解的几何结构类似于纠错编码,得到了严格的数学保证。
Jul, 2017
通过使用 Davis-Putnam 算法,提出了一种算法 CDP,用于计算 CNF 或 DNF 公式的模型的准确数量,该算法的平均运行时间是 O (nm^d),在大量的 CNF formulas 实验中的实际表现已经被估计。
Jun, 2011
本文介绍了优先变量,非优先变量,以及计算仅涉及优先变量的模型计数问题,探讨了三种不同的计数方法,并在多组实验结果上进行了比较。
Jul, 2015
本文提出了一种使用中国剩余定理将整数因子分解问题转化为 SAT 问题的算法,能够生成与 100 位整数因子分解一样难度的约 5600 变量的 SAT 实例。
Sep, 1998
介绍了一种基于 SAT 求解器的算法和实现工具,用于处理大规模的 CNF 公式的近似计数问题。通过多项式调用的方式,能够高精度地估算满足条件的解数,同时针对过大的问题仍能提供高置信度的估算边界。
Jun, 2013
模型计数、近似计数算法、可审核的近似计数器、证书和 oracle
Dec, 2023
该研究提出了一种基于单词级哈希函数的模型计数方法,可以直接利用复杂的 SMT 求解器,为概率推理中的计数问题提供了新思路。
Nov, 2015
本文研究了使用稳定模型语义进行推理的问题,提出了两种基于未建立的集合检测的实现技术,扩展了命题模型计数器到稳定模型计数器,可以在时间和空间使用方面显著优于现有的解决方案。
Nov, 2014
我们提出了第一个准确的伪布尔模型计数器 PBCount,它通过代数决策图的知识编译方法来实现。我们的实证评估表明,PBCount 可以计算 1513 个实例的计数,而当前最先进的方法只能处理 1013 个实例。我们的工作为进一步研究伪布尔公式的模型计数提供了几个方向,如预处理技术的开发和除知识编译之外的其他方法的探索。
本文介绍了一种使用浓缩哈希算法来加速模型计数问题的近似计数算法,实验结果表明使用浓缩哈希算法可以显著提高算法的速度。
Apr, 2020