Tseitin算法

Tattoo

发布日期: 2020-06-28 12:56:37 浏览量: 145
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/swy_swy_swy/article/details/104502127

Tseitin算法是一个在线性时间内将命题公式转化为CNF范式的算法。

例子:使用 Tseitin 算法将以下命题公式转化为 CNF 范式

上述公式等价于:

Tseitin算法

为每个非原子子式引入一个新变量:

将上述每个等价式转换为 CNF:

最后将T1T_1与转换后的CNF进行合取,得到最终的CNF:

F1F_1F4F_4其实就是第二步(就是T在箭头左边那些式子)的等价变形。

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

93
文章数
34
评论数
最近文章
eject