how to convert a propositional logical tree into conjunction normal form (CNF) tree
c, c++, conjunctive-normal-form, prefix-tree, recursion
Solution
Let's say you name your function `CNF`, taking a tree and returning the tree in CNF.
First, replace equivalency `p<=>q` with `AND(p=>q,q=>p)` then replace implications `p=>q` with `OR(q,NOT(p))`.
Convert to negation normal form: move all `NOT` operations down the tree, so that the `NOT` operations bind only to atoms (`A`, `B`).
Then, the result of `CNF(AND(x,y))` is simple: `AND(CNF(x),CNF(y))`, as it is CNF-like to have `AND`s high in the tree.
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.
Problem
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?