2.1.1 命题逻辑
命题逻辑下的公式由逻辑常量（true 和 false）、命题变量（表示为斜体小写字母，如 x、y、z）和逻辑联接词（否定、合取）组成。本文记公式中出现的变量的集合为 Vars()。任意变量集 X 上赋值是从 X 到{true, false}的映射，X 上所有赋值的集合记为 2X。给定公式以及 X 上的赋值，其中 Vars() X，满足递归定义如下：
（1）满足 true；
（2）不满足 false；
（3）满足 x 当且仅当x true ；
（4）满足当且仅当不满足；
（5）满足 当且仅当满足和满足。
给定公式和，若对于 Vars() Vars()上的任意赋值满足都有满足，则称蕴含，与等价（记为 ）当且仅当与相互逻辑蕴含。等价于常量 true 或 false 的公式称为平凡（trivial）公式。给定公式，Vars()上满足的赋值称为的模型，的所有模型的集合记为 M()，是可满足的（satisfiable）当且仅当 M() ，是有效的（valid）当且仅当 M() 2Vars()。给定任意赋值，其中赋值为 false 的变量数称为的度（cardinality）。给定公式，若其可满足，则的最小度定义为 M()中所有元素的度的最小值，否则定义为。为了方便，本文还将使用到如下五个逻辑联接词（其定义如表 1.1）：析取、条件、反条件、双条件和决策 ITE（表示“if . then . else .”）。任意公式的大小为||表示公式中使用的逻辑联接词的数目。
表 2-1 逻辑联接词
名称 | 定义 |
析取 | ( ) |
条件 | |
反条件 | |
双条件 | ( ) ( ) |
决策 ITE | ITE(, ,) ( ) ( ) |
在下文中，我们将使用到如下特定类型的公式：
（1）文字（literal）：变量 x（正文字）或其否定x（负文字）。给定文字 l，若 l x，则其否定文字l 为x，否则其否定文字为 x， l 与l 称为互补的文字。给定不含互补文字的文字集 L，下文记 Vars(L)
{x: x L 或x L}，记(L) {x false : x L} {x true : x
L}。给定赋值，下文记 L() {x: x false } {x: x true
}；
（2）子句（clause）：多个文字的析取，在明确上下文中子句有时亦表示为文字的集合，相反，给定文字集 L，在非明确上下文中我们使用(L)表示 L 中所有文字的析取组成的子句；
（3）项（term）：多个文字的合取，在明确上下文中项有时亦表示为文字的集合，相反，给定文字集 L，在非明确上下文中我们使用
(L)表示 L 中所有文字的合取组成的项；
（4）合取范式（conjunctive normal form，CNF）：多个子句的合取，有时亦表示为子句的集合，所有子句中文字数为 k 的 CNF 公式记为k-CNF 公式，其中 k 为常数；
（5）析取范式（disjunctive normal form，DNF）：多个项的析取，有时亦表示为项的集合；
（6）否定范式（negation normal form，NNF）：否定运算符只出现在变量之前的公式，显然，任意 CNF 和 DNF 公式都为 NNF 公式。
任意命题公式可表示为有根的有向无环图，每个终止节点标记为常量或变量，非终止节点标记为逻辑联接词，然后相同的子公式可合并为一个节点从而节省空间开销。