命题公式转CNF和CNF转DNF算法

一.命题公式转CNF：

1.去蕴含->：(将所有形如前式的换成后式，大写字母代表一个命题公式，小写字母表示原子，下同)

P -> Q        =>      ( ~P ) | ( Q );

2.转成NNF:(即将~全部转移到原子前)

~( P | Q )    =>      (~P) & (~Q);

~( ~P )        =>      P;

~( P & Q )   =>      (~P) | (~Q);

3.转化成CNF

(Q&R)|P      =>      (Q|P)&(R|P);

Q|(R&P)      =>      (Q|R)&(Q|P);

4.吸收

此时公式已转化成形如Q&Q1&Q2&...形式；

检查每个Q:

a|a   => a;

a|~a => true;

再检查各个Q之间是否包含，形如Qn=Qm|P；则删掉Qn，留Qm；

此时得出的结果就是吸收过的CNF了。

二.CNF转DNF:

CNF形如：

(a11|a12|a13..a1n)&(a21|a22...a2n)...(an1|an2...ann)

则对应的DNF为：

所有(a1,a2,a3...an)的析取(此处ai表示从ai1,ai2..ain中任取一个)；

对DNF进行吸收

此时公式已转化成形如Q|Q1|Q2|...形式；

检查每个Q:

a&a   => a;

a&~a =>false;

再检查各个Q之间是否包含，形如Qn=Qm&P；则删掉Qn，留Qm；

注;转DNF是会发生指数级膨胀，敝人对这个情况的处理也不清楚，可参考维基百科的cnf介绍

http://en.wikipedia.org/wiki/Conjunctive_normal_form

//我觉着它也没什么好办法。。。新添加原子貌似略坑啊。。。希望有高人看明白的或者另有好的办法处理这的能留言告知~不胜感激~

后来看到一个越南人论文实现的办法，挺靠谱的，如果任意公式则进行上面转cnf的1和2步，如果cnf转dnf则不需要1和2步处理；

第3步改变规则

3.转化成DNF

(Q|R)&P      =>      (Q&P)|(R&P);

Q&(R|P)      =>      (Q&R)|(Q&P);

这样就不会有之前cnf膨胀转dnf的问题。