如何将命题逻辑树转换为合取范式（CNF）树

Question

我有一个像字符串的字符串

     s="(=> P (OR (AND A (NOT B)) (AND B (NOT A))))";

并将其转换为该字符串的CNF，例如

（或（非P）（或AB））（或（非P）（或（非B）（非A）））

我需要构造一个TreeTree来保留值吗？

     struct TreeNode {
            string val;         // The data in this node.
            TreeNode *left;   // Pointer to the left subtree.
            TreeNode *right;  // Pointer to the right subtree.
            //TreeNode *farther;//should I use farther or not in convert to CNF?
      };

如何使它成为合取范式的CNF？请提供一些算法细节。从我的角度来看，也许使用递归函数可以更好地解决此问题，但是我仍然想不出如何使用递归。或者您有解决此问题的其他建议？

Answer 1

假设您将函数命名为CNF，获取一棵树并在 CNF 中返回该树。

1. 首先，将等效性替换为p<=>q，AND(p=>q,q=>p)然后将含义替换p=>q为OR(q,NOT(p))。

2. 转换为否定范式：将所有NOT操作沿树向下移动，以便NOT操作仅绑定到原子 ( A, B)。

3. 然后，结果CNF(AND(x,y))很简单： ，因为s 在树的高处AND(CNF(x),CNF(y))是类似 CNF 的。AND

4. 结果CNF(OR(AND(x,y),z))有点复杂。这里我们将使用析取大于合取的分布规则，这OR(AND(x,y),z)相当于AND(OR(x,z),OR(y,z))。实际上，CNF(OR(AND(x,y),z))将是AND(OR(CNF(x),CNF(z)),OR(CNF(y),CNF(z)).

你就完成了。