如何将命题逻辑树转化为合取范式树

Question

我有一个string

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

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

(OR (NOT p) (OR A B))(OR (NOT P) (OR (NOT B) (NOT A)))

我需要做一个结构体TreeNode来保持值吗?

     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. 首先用AND(p=>q,q=>p)代替等价的p<=>q，然后用OR(q,NOT(p))代替含义的p=>q。

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

3. 然后，CNF(AND(x,y))的结果很简单:AND(CNF(x),CNF(y))，因为它是CNF-like将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))。

Answer 2

简单递归下降解析器解决方案:

TreeNode* ParseExpression(const char*& p):如果p指向的字符串不是以'('开头的，则返回ParseAtom(p)，否则将p移过'('，调用ParseOperation(p)，然后将p移过')'并返回由ParseOperation返回的值。

TreeNode* ParseAtom(const char*& p):跳过原子(连续的非空格序列)。返回一个以原子为值的TreeNode，左右为NULL。

TreeNode* ParseOperation(const char*& p): p所指向的字符串应该以操作符开始。将p移过运算符，然后确定运算符使用了多少个操作数。如果有，调用ParseExpression(p)一次;如果有两个，调用ParseExpression(p)两次。然后返回一个TreeNode，操作符作为值，一个或两个ParseExpression调用的结果作为左和右(对于只有一个操作数的操作符，右应该为NULL)。

设置指向原字符串的指针;在指针上调用ParseExpression;返回值是您的树，指针将指向字符串中的第一个表达式。

这解决了你的一个问题:如何将字符串转换为树。Adrian Panasiuk解决了另一个问题，如何将树转换为标准形式。由于您将进行额外的树转换，因此节点中的"值"应该称为"op"或类似的名称，以表示"操作符"(这是c++中的保留字)，并且它应该是enum，而不是字符串。