模型计数（model counting,#SAT）问题是人工智能领域的一个基本问题,旨在求解给定命题公式的可满足赋值个数,求解难度是#P完全的。现代基于CDCL（conflict driven clause learning）框架的模型计数求解器已经能够处理具有百万条子句的大型合取范式（conjunctive normal form,CNF）。然而,在诸如贝叶斯网络、规划、有界模型检测、概率推理等复杂实际应用中,仍有许多庞大的CNF公式使用目前最先进模型计数求解器也难以求解。对于大规模问题而言,简化CNF公式中的子句,是提升模型计数求解效率的有效方法。模型计数的预处理阶段能够通过使用命题公式推理规则删除冗余子句和变量,实现对命题公式中子句的简化。包含消除（subsumption elimination,SE）、重言式消除（tautology elimination,TE）、活化（vivification,VIV）、B+E算法等多种先进的预处理技术能够大大减少了命题公式的子句数。然而子句简化后的命题公式并非总能在模型计数时表现得更好,存在部分反常公式经预处理后模型计数总时间反而明显增加。本文提出衡量预处理前后命题公式模型计数求解难度的标准,通过判断预处理后命题公式是否更难求解实现对反常公式的过滤。本文提出预处理筛选算法FILTER,通过调用PMC和B+E两种成熟的预处理器,对比原公式以及两种预处理后公式的求解难度,筛选出求解难度最低的公式进行模型计数。在最新的精确模型计数求解器Exact MC上测试算法FILTER,实验结果表明本文提出的预处理筛选策略综合了PMC和B+E的好处,从整体上提高了模型计数求解效率。在许多大规模实际问题中,多值变量的出现十分常见。多值变量在命题逻辑知识库中表示为exactly-one约束,在使用模型计数解决包含多指变量的实际问题时,通常需要将exactly-one约束转换为CNF公式,这将以指数形式扩大CNF公式的子句规模,容易造成模型计数求解时间溢出的问题。为更好地解决这类问题,本文提出了从CNF公式中识别exactly-one约束的算法ECR。C2D是目前唯一能够直接处理exactly-one约束的求解器,实验结果显示算法ECR显著提升了C2D的求解效率。对于其他不能直接处理exactly-one约束的模型计数求解器,本文提出对exactly-one约束进行单独处理的算法ECP。将算法ECR和算法ECP应用于模型计数求解器Exact MC,改进得到的模型计数求解器ECMC性能优于Exact MC。综上,本文的主要研究内容是通过简化命题公式的子句,提升模型计数求解效率。在对模型计数问题中命题公式的子句进行简化时,本文采用了两种策略:一是在预处理阶段过滤反常公式的预处理筛选策略,二是在求解阶段识别和单独处理命题公式中exactly-one约束的策略。在Exact MC和C2D两种模型计数求解器上测试的实验结果表明,本文提出的两种策略都实现了命题公式的简化和模型计数求解效率的提升。