I know the 4 rules to convert the formulas to CNF, but I'm not quite sure how to apply them to this formula ((x v y) ^ ¬ z) ->w
Could someone give me a hand and a bit of an explanation? Thanks!
Recipe for converting an expression into CNF
One way to convert a formula to CNF is:
This recipe can be made plausible as follows:
None of the clauses must be false, unless the overall expression is false. Therefore, every clause is representing a minterm of the inverted expression. To make sure that this term is false, none of the inverted literals can be true.
For n input variables, a truth table has 2^n terms. Therefore, this method is only practical for small expressions.
To demonstrate the steps with your sample formula
((x or y) and not z) implies w
Truth table (F = expression value):
wxyz|F
----+-
0000|1
1000|1
0100|0
1100|1
0010|0
1010|1
0110|0
1110|1
0001|1
1001|1
0101|1
1101|1
0011|1
1011|1
0111|1
1111|1
----+-
False terms (F = 0):
wxyz|F
----+-
0100|0
0010|0
0110|0
----+-
Literals inverted and output column omitted:
wxyz
----
1011
1101
1001
----
Resulting CNF clauses:
(w or !x or y or z) and (w or x or !y or z) and (w or !x or !y or z)
Resulting CNF clauses minimized by merging clauses:
(w or !x or z) and (w or !y or z)
If in doubt, you can ask Wolfram|Alpha.
From the Karnaugh map, it becomes clear how the three false terms can be merged into two clauses:
wx
00 01 11 10
+---+---+---+---+
00 | 1 | 0 | 1 | 1 |
+---+---+---+---+
01 | 1 | 1 | 1 | 1 |
yz +---+---+---+---+
11 | 1 | 1 | 1 | 1 |
+---+---+---+---+
10 | 0 | 0 | 1 | 1 |
+---+---+---+---+