Convert prop. logic to DNF

Question

Q: d&(a<->d)&c|((b|b)&!d<->!c|(b<->d))

SNF with d (DNF form):

!d&!(b<->!c&!b)|d&(a&c|(c|!b))

SNF with b:

!b&(d|c&!d|!a)|b&(a&c|c)

SNF with c:

c&(!b|b&a)|!c&b|!d

SNF with a:

!a&!c|b&c|!b&d|a&c|!c&b|!d

It seems I'm unable to reach any closer to the answer : a&b&c&d|b&!c&!d|c&d&!b

How can I uncomplicate this process?

Answer 1

Maybe like this?

Note that we have (x⇒φ|ψ) ⇔ (¬x ∧ ψ) ∨ (x ∧ φ)

    d&(a<->d)&c|((b|b)&!d<->!c|(b<->d))
    <=> ¬d∧(0&(a<->0)&c|((b|b)&!0<->!c|(b<->0))) ∨
         d∧(1&(a<->1)&c|((b|b)&!1<->!c|(b<->1)))
    <=> ¬d∧(b<->!c|!b) ∨
         d∧(a&c|!(!c|b))
    <=> ¬d∧(¬b∧(0<->!c|!0) ∨ b∧(1<->!c|!1))) ∨
         d∧(¬b∧(a&c|!(!c|0)) ∨ b∧(a&c|!(!c|1)))
    <=> ¬d∧(¬b∧!(!c|1) ∨ b∧(!c))) ∨
         d∧(¬b∧(a&c|c) ∨ b∧(a&c))
    <=> ¬d∧b∧!c ∨
         d∧(¬b∧c ∨ b∧a&c)

    <=> ¬d∧b∧!c ∨ d∧¬b∧c ∨ d∧b∧a∧c

Comments

I see, I was applying the Cannonical DNF form instead on the implication after SNF.