Ex 5_33 实现一个关于公式长度(其中所有文字总的出现次数)为线性时间的Horn公式可满足性问题_第十次作业

       对于所有的蕴含式,生成一张有向图,对于每一个蕴含式,将左边的每一个文字连接到一个中间结点,并用中间结点记录蕴含式左边文字的数量,然后将中间结点连接到蕴含式的右侧结点。例如,对于蕴含式集合

生成的有向图如下

然后将所有的文字的设为false,从某一个值为0的中间结点开始做深度优先遍历,将中间结点所连接的文字设为true,并将这些文字所指向的中间结点的值减1,如果有某个中间结点减去1后为0, 说明指向中间结点的文字都为true,要满足蕴含式,则需把中间结点指向的结点的值设为true,即继续在这个中间结点上做深度优先遍历,直到不能找到值为0的中间结点为止。这个时候文字的取值可以满足所有的蕴含式,接下来继续判断是否满足所有的纯否定句即可。

原文地址:https://www.cnblogs.com/xiu68/p/7988834.html