Equation to CNF

Question

While converting following equation to CNF form, I resolved one part, but the other part (yellow) there is mistake, can you give a hint:

x <-> (y1 <-> y2)

x <-> { (y1->y2) & (y2->y1) }

x <-> { (!y1 | y2) & (!y2 | y1) }

[ x -> { (!y1 | y2) & (!y2 | y1) } ] 
  & [{ (!y1 | y2) & (!y2 | y1) } -> x]

[ !x | { (!y1 | y2) & (!y2 | y1) } ] 
  & [! { (!y1 | y2) & (!y2 | y1) } | x]

[ {!x | (!y1 | y2)} & { !x | (!y2 | y1) } ] 
  & [{ !(!y1 | y2) | !(!y2 | y1) } | x]

(!x | !y1 | y2) & (!x | !y2 | y1) 
  & [{ (y1 & !y2) | (y2 & !y1) } | x]

(!x | !y1 | y2) & (!x | !y2 | y1) & [ (y1 & !y2) | (y2 & !y1) | x]

Answer 1

Well. I wouldn't call this a mistake. But one thing that I would have done differently is the transformation of the inner ↔. For the outer one, you picked the CNF version. It generated two copies of the inner ↔. One with a negation, one without a negation. By replaying the inner ↔, one copy stays a CNF, the other one becomes a DNF. If you chose the DNF for the negated inner ↔, the negation would transform it to a CNF and your life would be easier.

Comments

Martin gave a good hint. One important thing to note is that you can replace equivalences and xors either by their CNF or DNF, i.e.,

    a <-> b
        = (!a | b) & (a | !b)
        = a & b | !a & !b

    a ^ b
        = (a | b) & (!a | !b)
        = a & !b | !a & b

While it does not matter in terms of correctness which replacement you choose, the one may make much more effor than the other. Therefore, choose wisely among the two when converting formulas to DNF or CNF.

For your formula, you can compute that as follows:

    x <-> (y1 <-> y2)
    = (!x | (y1 <-> y2)) & (!(y1 <-> y2) | x)
    = (!x | (y1 <-> y2)) & ((y1 ^ y2) | x)
    = (!x | (!y1 | y2) & (y1 | !y2)) & ((y1 | y2) & (!y1 | !y2) | x)
    = (!x | !y1 | y2) & (!x | y1 | !y2)) & (y1 | y2 | x) & (!y1 | !y2 | x)