2.1.4 模型计数
模型计数问题是 SAT 问题的重要扩展，该问题旨在计算满足公式的赋值的数量。模型计数问题相较于 SAT 问题更具有挑战性，具有#P 完全的计算复杂性。总体而言，模型计数方法可分为精确和近似两大类。随着模型计数应用需求的持续增长以及学界对模型计数相关算法研究的不断深入，再加之模型计数竞赛[10]的推广，领域中已出现了数十种模型计数求解器。
精确求解算法主要分为三类：基于搜索、基于编译以及基于变量
消元。基于搜索的模型计数方法的主要思想是通过更智能的枚举部分 解来扩展 DPLL 框架[33] 。开创性的基于搜索的模型计数求解器是 Cachet[34] ，它首先实现了将组件（子句的子集）缓存与冲突驱动的 子句学习相结合来进行模型计数。随后的模型计数求解器sharpSAT[35] 改进了组件缓存方案以及决策启发式。在sharpSAT 的基础上，Ganak[36]进一步引入了概率缓存。考虑到 Cachet、sharpSAT 和 Ganak 按照 Decision-DNNF[37] 进行搜索,可扩展模型计数器 ExactMC[38] 按照 Decision-DNNF 的泛化表示进行搜索,实验结果表明能明显著提高求解效率。 最近的 SharpSAT-TD[39] 在 sharpSAT 的基础上使用 FlowCutter 算法计算输入公式的树分解，并将树分解应用到决策启发 式中，在 2021 年的模型计数比赛中取得了冠军。基于编译的技术依 赖于高效的知识编译器，编译器将输入语言表示的公式编译为目标语 言表示的公式，编译后可以使用目标语言的表示高效地进行模型计数。例如，可以将公式转换为二元决策图并从标记为 1 的叶节点开始一直 遍历到根节点以读取解的数量。c2d[41] 就是一个著名的基于编译的模 型计数求解器，它将给定的合取范式公式转换为可分解的否定范式, 而该范式是有序二元决策图的严格超集，并且通常更简洁.其他有代 表性的模型计数求解器还有 Dsharp[42] 、miniC2D[43] 和 d4[44] 等。基 于变量消除的方法将问题表述为，并通过对变量进行一系列相乘、映 射来执行模型计数。ADDMC[45] 是一个具有代表性的基于变量消除 的模型计数求解器，它的主要思想是使用代数决策图来执行相乘、映 射操作。随后，研究人员提出了一个统一的动态规划框架，称为 DPMC[46] ，ADDMC 可以视为 DPMC 的特例。在 DPMC 框架中,公 式的模型计数是对公式构建项目连接树后计算得到。
近似模型计数算法根据提供的近似保障可进一步分为三类。第一类是提供(, )近似保证的近似求解器，假设真实模型数为 Z，则求解器能在 1的概率内输出介于[Z/(1+)，Z(1+)]的估计值，代表性的求
解器为 ApproxMC[47] 。第二类求解器提供一定概率下的上界或下界保证，代表性的求解器包括 MBound[48] 和 SampleCount[49] 。第三类不提供任何保证，但在实际应用中可扩展性最强，代表性的求解器为satss[50] 和 STS [51] 。
目前国内开展模型计数研究的单位包括吉林大学、中科院软件所、东北师范大学、暨南大学等。