可满足性与范式
称是可满足式(Satisfiable),当且仅当存在某些解释使得公式的取值.
使公式取值为真的解释称为的模型(Model).
称是永真式(Tautology),当且仅当所有的解释均使公式的取值为真,记作.
称是永假式或不可满足式(Unsatisfiable),当且仅当所有的解释均使公式的取值为假,记作.
称是可为假式(Falsifiable),当且仅当存在某些解释使得公式的取值.
例:是不可满足式。
设为一个公式集合,称是可满足的,当且仅当存在一个解释使得对于所有的,, 该解释称为的模型。
称是不可满足的,当且仅当对于所有的,.
令为一个公式集合,为一个公式。称是的逻辑后果(Logical Consequence),当且仅当的每一个模型也是的模型。记作.
由有限个命题变量或其否定所组成的合取式称为基本积。
例如: , , 都是基本积。
由有限个命题变量或其否定所组成的合取式称为基本和。
例如: , , 都是基本和。
, 既是基本积,也是基本和。
一个由基本积的析取组成的命题公式,称为析取范式(Disjunctive Normal Form, DNF),即该命题公式具有形式:
其中都是基本积。
例如: 命题公式是析取范式。
一个由基本和的合取组成的命题公式,称为合取范式(Conjunctive Normal Form, CNF),即该命题公式具有形式:
其中都是基本和。
例如: 命题公式是合取范式。
和既是析取范式,也是合取范式。
定理:(范式存在定理)任何命题公式都存在与其等值的析取范式和合取范式。
任何命题公式的析取范式和合取范式不一定是唯一的。
对于一个命题公式,求其析取范式和合取范式的步骤如下:
(1)消去{}以外的逻辑联结词;
(2)利用德摩根律将否定联结词内移,消去双重否定;
(3)利用分配律将公式化成析取范式或合取范式。
例:求下面命题公式的合取范式:
解:
利用析取范式和合取范式可对命题公式的可满足性进行判定。
(1) 一个析取范式是永假式,当且仅当它的每个基本积都是永假式。
(2) 一个合取范式是永真式,当且仅当它的每个基本和都是永真式。
(3) 一个命题公式为永假式当且仅当它的析取范式中每一个基本积都至少含有一个命题及其否定。
(4) 一个命题公式为永真式当且仅当它的合取范式中每一个基本和都至少含有一个命题及其否定。
在含有个命题变量的基本积中,如果每个命题变量与它的否定不同时存在,但二者之一必出现且仅出现一次,则这样的基本积称为极小项。
例如: , .
在含有个命题变量的基本和中,如果每个命题变量与它的否定不同时存在,但二者之一必出现且仅出现一次,则这样的基本和称为极大项。
例如: .
对于给定的含个命题变量的命题公式,若其析取范式的基本积均是这个命题变量的极小项,则称该析取范式为命题公式的主析取范式。
基本形式:
定理:(主析取范式存在唯一性)任何不为永假式的命题公式都存在与其等价的主析取范式,且唯一。
对于给定的含个命题变量的命题公式,若其合取范式的基本和均是这个命题变量的极大项,则称该合取范式为命题公式的主合取范式。
基本形式:
定理:(主合取范式存在唯一性)任何不为永真式的命题公式都存在与其等价的主合取范式,且唯一。
求主范式可采用真值表法
在真值表中,命题公式真值为的解释所对应真值为的极小项的析取,即为该命题公式的主析取范式。
在真值表中,命题公式真值为的解释所对应真值为的极大项合取,即为该命题公式的主合取范式。
可以按以下步骤构造主析取范式:
(1)将命题公式化为析取范式;
(2)除去析取范式中所有永假的基本积;
(3)利用等幂律将重复出现的基本积和基本积中重复出现的变量合并;
(4)利用同一律在基本积中补入未出现的命题变量(如),然后用分配律展开;
(5)再次利用等幂律将重复出现的极小项合并。
例:求的主析取范式。
解: