c++crecursionconjunctive-normal-formprefix-tree

how to convert a propositional logical tree into conjunction normal form (CNF) tree


I have a string like string

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

and convert it output the CNF of this string,like

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

do I need to make a struct TreeNode to keep the value?

     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?
      };

how to make it to CNF, which is conjunctive normal form? please give some algorithm detail. from my point of view, maybe use recursive function is better for solving this problem, but I still can not think out how to use recursion. Or you have other suggestion for solving this problem?


Solution

  • Let's say you name your function CNF, taking a tree and returning the tree in CNF.

    1. First, replace equivalency p<=>q with AND(p=>q,q=>p) then replace implications p=>q with OR(q,NOT(p)).

    2. Convert to negation normal form: move all NOT operations down the tree, so that the NOT operations bind only to atoms (A, B).

    3. Then, the result of CNF(AND(x,y)) is simple: AND(CNF(x),CNF(y)), as it is CNF-like to have ANDs high in the tree.

    4. The result of CNF(OR(AND(x,y),z)) is a little bit more complicated. Here we will use the rule of distribution of disjunction over conjunction, which is OR(AND(x,y),z) is equivalent to AND(OR(x,z),OR(y,z)). In effect, CNF(OR(AND(x,y),z)) will be AND(OR(CNF(x),CNF(z)),OR(CNF(y),CNF(z)).

    And you're done.