1 基本概念
合取范式是逻辑表达式的一种常见标准形，用于将复杂公式组织为便于分析和处理的结构。它的核心特点是：整体由若干部分通过“与”连接，而每个部分内部再由若干文字通过“或”连接。由于这种层次分明的形式，CNF 在逻辑演算、程序验证和自动推理中都十分常见。
1.1 定义
合取范式通常指一个公式写成若干子句的合取，其中每个子句是若干文字的析取。若将“与”视为外层连接，“或”视为内层连接，则该表达式即呈现典型的 CNF 结构。对于命题逻辑与谓词逻辑，CNF 的具体定义略有差别，但基本思想一致，即把公式整理成“子句的集合”形式。
1.2 组成元素
合取范式的构成可分为三个层次：文字、子句与合取结构。它们共同决定了公式的外观和可操作性。
1.2.1 文字
文字是最基本的逻辑单位，通常指一个命题变元或其否定；在谓词逻辑中，也可理解为原子公式及其否定。文字本身不再含有更低层次的逻辑连接，是构成子句的最小材料。
1.2.2 子句
子句由一个或多个文字通过析取连接而成。一个子句可看作“至少有一个文字为真”时成立的条件。若子句中包含互为否定的文字，则它通常恒真；若不包含任何文字，则形成空子句，常用于表示矛盾。
1.2.3 合取结构
多个子句通过合取连接后，就形成完整的 CNF。这样的结构表示所有子句都必须同时成立，因此外层的“与”具有约束作用，而内层的“或”则提供局部的选择空间。
1.3 与析取范式的关系
合取范式与析取范式是两种对偶的标准形式。析取范式以“或”连接若干合取项，而合取范式则以“与”连接若干析取子句。二者在表达能力上等价，理论上可相互转换，但在实际计算中，CNF 更适合作为统一输入格式，因而更常用于自动推理和可满足性求解。
2 形式化表示
CNF 的形式化表示依赖于所讨论的逻辑系统。命题逻辑中的表示较为直接，而谓词逻辑中的表示通常还需要处理量词、变量和项结构。
2.1 命题逻辑中的合取范式
在命题逻辑中，CNF 由若干子句的合取组成，每个子句是命题文字的析取。其表达简洁明确，适合用作算法输入。
2.1.1 标准结构
命题逻辑 CNF 的标准结构可写为： \[ (C_1 \land C_2 \land \cdots \land C_n) \] 其中每个 \(C_i\) 都是若干文字的析取。若将公式视为子句列表，则每一项都代表一个独立约束。
2.1.2 允许的连接词
在纯粹的 CNF 中，通常只允许使用合取、析取和否定，其中否定仅作用于原子命题。也就是说，否定应被推到最内层，不能直接作用于复合公式。这样可以保证表达式保持规范化。
2.2 谓词逻辑中的合取范式
在谓词逻辑中，CNF 往往以子句集合的方式出现，并伴随量词前置、变量重命名和斯科伦化等步骤。与命题逻辑相比，它多了对结构和绑定关系的处理。
2.2.1 量词前束化
量词前束化是将所有量词尽量移到公式前端，形成统一的量词前缀。这样做可以把主体部分简化为不含量词的矩阵，为后续转化为子句形式创造条件。
2.2.2 子句化表示
谓词逻辑中的 CNF 常表示为若干子句的合取，每个子句内包含若干带变量的文字。经过标准化后，量词信息通常被隐含在前缀中，而主体则以子句集合的形式呈现。
2.3 规范化与等价变形
CNF 的规范化通常依赖一系列保持逻辑意义或保持可满足性的变形。若要求严格等价，则每一步都必须保持公式真值不变；若只要求可满足性保持，则允许通过引入新符号等方式进行更高效的转化。不同场景下对“规范”的要求并不相同。
3 转换方法
将任意公式转换为 CNF，通常要按步骤处理逻辑连接词、否定位置、变量冲突和分配结构。这一过程既是形式化操作，也是算法实现中的核心环节。
3.1 消去蕴含与等值
转换的第一步通常是消去蕴含、等值等派生连接词。例如，蕴含可改写为析取形式，等值可拆分为两个方向的蕴含。这样可将公式还原为只含基本连接词的形式，便于后续整理。
3.2 否定内移
否定内移是把否定符号尽量向公式内部推进，直到只作用于原子公式为止。该步骤通常借助德摩根律以及双重否定消去完成。完成后，公式中不会再出现作用于复合结构的否定。
3.3 变量标准化
在谓词逻辑中，不同量词所绑定的变量必须避免重名干扰，因此需要先进行变量标准化。也就是说，重名变量会被改写为彼此不同的符号，以保证后续变形不会混淆变量作用域。
3.4 分配律展开
当公式已经只含有基本连接词后，就需要通过分配律将析取与合取调整为 CNF 所要求的层次结构。这一步通常是从析取向合取分配，以把表达式改写为子句合取的形式。
3.4.1 对析取的分配
典型做法是将一个析取项分配到合取结构中，例如把 \(A \lor (B \land C)\) 改写为 \((A \lor B) \land (A \lor C)\)。通过反复应用这一规则，能够把表达式逐步展开为合取若干子句的形式。
3.4.2 对合取的整理
在分配完成后，常需重新整理括号与层次，使得外层保持合取，内层保持析取。若出现嵌套合取，可将其平铺；若某些子句结构重复，也可在整理时合并处理。
3.5 去重与简化
最终得到的 CNF 往往还要进行去重与简化，例如删除重复文字、消去恒真子句、移除包含关系明显的冗余子句等。这些操作不改变基本语义，却能显著降低公式规模，提高后续求解效率。
4 性质
CNF 之所以重要，不仅因为它形式整齐，还因为它具有适合算法处理的一系列性质。许多逻辑问题一旦进入 CNF，就更容易归结为统一的搜索或推导过程。
4.1 逻辑等价性
通过适当的规则变换，原公式可以被改写为与其逻辑等价的 CNF。对于命题逻辑，这种等价转换通常是直接成立的；对于谓词逻辑，则常在前束化和斯科伦化后保留特定意义上的等价或可满足性等价。
4.2 可满足性保持
在自动推理中，很多时候只关心原公式是否可满足，而不要求与变换后公式完全等价。CNF 转换常被设计为可满足性保持，即原公式可满足当且仅当其转化结果可满足。这使得求解器能够在不损失答案正确性的前提下工作。
4.3 唯一性与非唯一性
CNF 的表达通常不是唯一的。同一公式可以通过不同的变换顺序、不同的变量命名方式，得到多种等价或可满足性等价的 CNF。也正因如此，CNF 更像一种规范框架，而非单一固定文本。
4.4 复杂度特征
从表达长度看，公式转 CNF 可能导致规模增长，尤其在分配律反复展开时，子句数会迅速增加。某些公式在转换后会出现指数级膨胀，这也是实际系统中常借助增量转换、共享结构或新引入辅助变量的原因。
5 应用
CNF 的应用范围很广，凡是需要统一逻辑表达、执行自动推理或进行组合搜索的场景，往往都会使用这种形式。
5.1 自动定理证明
在自动定理证明中，公式常被转化为子句集合，再通过归结、消解或其他推理规则进行演算。CNF 为这些过程提供了统一输入，使证明步骤更容易机械化实现。
5.2 SAT 求解
布尔可满足性问题通常直接以 CNF 作为标准输入格式。现代 SAT 求解器普遍围绕 CNF 设计，通过冲突分析、回溯与传播等机制判断公式是否存在满足赋值。
5.3 逻辑电路设计
在数字电路设计与验证中，逻辑关系常被映射为 CNF，以便检查电路行为是否符合预期。某些硬件验证任务会把门级电路转换成子句约束，再交由求解器处理。
5.4 知识表示与推理
知识库中的规则与事实可以整理成 CNF 形式，以便进行一致性检查、结论推导和冲突检测。由于子句结构明确，系统更容易维护和更新知识条目。
5.5 约束满足问题建模
许多组合约束可以转写为 CNF，从而借助 SAT 技术求解。例如排程、配置选择和某些图问题，都可通过引入命题变量并编码约束的方式纳入统一框架。
6 相关概念
CNF 与多种逻辑概念密切相关。理解这些概念，有助于把握其在逻辑系统中的位置。
6.1 析取范式
析取范式是 CNF 的对偶形式，由若干合取项通过析取连接而成。它与 CNF 同样属于标准化表达，但在算法使用上不如 CNF 普遍。
6.2 子句范式
子句范式强调公式以子句集合来表示，是 CNF 在逻辑推理中的常用别称或近似表述。在许多文献里，子句范式与合取范式几乎可以互换理解。
6.3 斯科伦标准形
斯科伦标准形是谓词逻辑中将存在量词消去后得到的形式，通常作为进一步转化为子句集合的基础。它与 CNF 密切相关，但更强调量词处理与函数符号引入。
6.4 互补文字与空子句
互补文字指一个文字与其否定的配对。若某子句同时含有互补文字，则该子句恒真；空子句则没有任何文字，通常表示不可满足或矛盾，是子句推理中的重要终止标记。
7 典型示例
通过示例可以更直观地理解 CNF 的结构及其转换过程。不同逻辑系统中的写法虽不相同，但核心方法一致。
7.1 命题公式示例
例如公式 \((p \lor q) \land (\neg r \lor s)\) 本身就是一个合取范式。它包含两个子句，分别是 \(p \lor q\) 与 \(\neg r \lor s\)，二者通过“与”连接。
7.2 谓词公式示例
对于谓词公式 \(\forall x\, (P(x) \lor Q(x)) \land \forall x\, (\neg P(x) \lor R(x))\)，其结构已经接近 CNF。若进一步整理变量与量词前缀，可将其视为两个子句的合取，每个子句内含带变量的文字。
7.3 规范化过程示例
考虑公式 \(A \lor (B \land C)\)。先应用分配律，可得 \((A \lor B) \land (A \lor C)\)。此时外层是合取，内层是析取，便完成了向 CNF 的转换。若再加入否定或蕴含，通常还需先执行消去与内移步骤，再进行分配展开。