formulaboolean-logicconjunctive-normal-form

How to convert formula to CNF?


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!


Solution

  • Recipe for converting an expression into CNF
    One way to convert a formula to CNF is:

    1. Write a truth table (only the terms are relevant where the formula evaluates to false)
    2. In every term of the truth table invert all literals
    3. Take the resulting terms as CNF clauses

    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 |
          +---+---+---+---+