投影模型计数
本文研究了使用稳定模型语义进行推理的问题，提出了两种基于未建立的集合检测的实现技术，扩展了命题模型计数器到稳定模型计数器，可以在时间和空间使用方面显著优于现有的解决方案。
Nov, 2014
介绍了一种基于 SAT 求解器的算法和实现工具，用于处理大规模的 CNF 公式的近似计数问题。通过多项式调用的方式，能够高精度地估算满足条件的解数，同时针对过大的问题仍能提供高置信度的估算边界。
Jun, 2013
本篇论文介绍了一种从 SMT 到 #SMT 近似版本的约简方法，并提出了关于整数算术和线性实数算术的模型计数算法，通过对现代 SMT 求解器的高级启发式算法进行利用，运行时间为多项式级别并提供正式边界。我们使用这些算法来解决带有非确定性的无循环概率程序模型的值问题。
Nov, 2014
我们提出了第一个准确的伪布尔模型计数器 PBCount，它通过代数决策图的知识编译方法来实现。我们的实证评估表明，PBCount 可以计算 1513 个实例的计数，而当前最先进的方法只能处理 1013 个实例。我们的工作为进一步研究伪布尔公式的模型计数提供了几个方向，如预处理技术的开发和除知识编译之外的其他方法的探索。
Dec, 2023
该研究论文探讨了如何通过增加短的随机奇偶约束来计算公式满足的真实赋值（模型），实现 NP 问题的计数，尤其是当需要添加多个约束时，随机奇偶约束的集合解的几何结构类似于纠错编码，得到了严格的数学保证。
Jul, 2017
本篇论文设计了一种基于部分知识编译的新型近似模型计数方法 PartialKC，其在可伸缩性和准确性方面都表现显著优于以前的近似计数器，并可以收敛于精确计数器，实验证明其具有精确计数器可比的性能。
Dec, 2022
研究了哈希算法在计算 Boolean 公式中的模型数量时，delta 值较小会对可伸缩性造成重大影响。提出了一种基于 Rounding 的新方法和一种新算法（RoundMC），用于高置信度下的估计，可以显著提高运行时性能。RoundMC 能够比当前技术水平更好地解决问题，速度提高了 4 倍。
May, 2023
本文介绍了一种新算法来解决投影模型计数（PMC）问题，该算法利用输入实例的原始图的小树宽，并在同时考虑了指标化的树宽有理论下限的情况下，提供固定参数可解，通过使用嵌套动态规划，并在数据库技术的帮助下，可以解决树宽上限超过 200 的实例的 PMC 问题和热门的 PMC 特殊情况＃Sat。
May, 2023