2.1.2 命题推理问题
命题知识库通常表示为命题公式，库中的知识表示为被该公式蕴含的所有公式，因此命题推理问题通常可表示为知识库的查询问题。本文中涉及到的推理问题如下：
（1）判定知识库的一致性，也即判定对应命题公式的可满足性。该问题的重要性主要来源于两方面。第一，不满足当且仅当 可满足，因此该问题在自动推理中处于核心位置。第二，SAT 问题是第一个被证明为 NP 完全的问题，其多项式时间的求解算法将导致所有 NP 中问题皆能在多项式时间求解。由于任意逻辑公式的可满足性问题都可转化为某个线性大小的 CNF 公式的可满足性问题，且 CNF公式的可满足性问题也是 NP 完全的，因此有时 SAT 问题也简单表示为 CNF 公式的可满足性问题，k-CNF 公式的可满足性问题相应称为 kSAT 问题。当 k 3 时，kSAT 问题是 NP 完全的，而 2SAT 问题为 NL 完全的。
（2）判定知识库的有效性。该问题与 SAT 问题互补，是 co-NP
完全的。
（3）判定知识库是否蕴含某个子句。由于任意公式都可表示为等价的CNF 公式，而知识库蕴含一个 CNF 公式当且仅当其蕴含 CNF中所有子句，因此任意表示语言是否支持多项式时间的子句蕴含判定算法是衡量该语言易处理性的最基本标准[14] [15] 。
（4）判定某个项是否蕴含知识库。该问题与子句蕴含判定问题互补，在基于模型的诊断领域有重要应用。
（4）计算知识库的模型数。CNF 公式的模型计数问题为#P 完全 问题，模型计数问题在人工智能和形式化验证领域具有众多应用场景，
例如，解决多种概率推理问题，如贝叶斯网络推理可以高效地转化为模型计数问题[16] ，文献[17] 提出的基于加权模型计数的贝叶斯推理方法是目前最快的精确贝叶斯推理方法.此外,模型计数还在自动规划
[18] 、神经网络验证[19] 等领域有着广泛的应用场景。
（5）枚举知识库的所有模型。该操作在产品配置中有重要应用，可用于枚举出所有满足用户需求的方案[20] 。
（6）判定知识库间的等价性。该问题在电子设计自动化领域有 重要应用，可用于确定两种电路设计是否表现出完全相同的行为[21] 。
（7）判定知识库间的蕴含关系。
（8）计算知识库的最小度。知识库的最小度在某些应用中代表明确的语义。例如，在基于模型的诊断中，最小度可表示给定可观察系统中最小的故障数；又如，在自动规划中，可用于表示得到指定目标所需的最少动作数[22] 。