Exercise 1: Question 2-part b

Question

I have a query regarding this task:
Transform to DNF:

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

When I am trying to solve this question, its getting complex and complex. I am attaching image of my attempt to solve this.

If anyone know any better method to solve this, please do comment.

Any assistance in this regard is highly appreciated.

Thank you!

Answer 1

It's a bad formula, but what about this solution using first Shannon decomposition on variable a:

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

Now let's focus on subformula !(b<->d)<->!(b|c) with a further Shannon decomposition on variable b:

    (!(b<->d)<->!(b|c))
    = (!(true<->d)<->!(true|c)) & b | (!(false<->d)<->!(false|c)) & !b
    = (!d<->false) & b | (!!d<->!c) & !b
    = d & b | (d<->!c) & !b
    = b&d | !b&!c&d | !b&c&!d

Hence,

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

Answer 2

What you did looks quite reasonable, and it is definitely a way to get there. You chose to convert the inner biimplications to DNF first and then tackle the outer ones. But eventually, you get to the point where you negate the DNFs and have mixed CNF and DNFs. That's starting to cause some trouble.

Let's look a the formula:
¬(b ↔ d∧a) ↔ (b∨c → ¬a) ↔ a
Let's look at the subformulas:
x1 := ¬(b ↔ d∧a)
x2 := (b∨c → ¬a)

Since we have these formulas inside the biimplications, we will need them both in a negated, and in an unnegated form. Also, we want to be able to use them as DNF or CNF depending on what fits better to the current occurrence.
x1 := ¬(b ↔ d∧a) = (¬b ↔ d∧a) = (¬¬b ∧ ¬(d∧a)) ∨ (¬b ∧ d∧a) = (b ∧ (¬d ∨ ¬a)) ∨ (¬b ∧ d ∧ a)
x1dnf := (b ∧ ¬d) ∨ (b ∧ ¬a) ∨ (¬b ∧ d ∧ a)
x1 = (¬b ↔ d∧a) = (¬b → d∧a) ∧ (d∧a → ¬b) = (b ∨ d∧a) ∧ (¬(d∧a) ∨ ¬b)
x1cnf = (b ∨ d) ∧ (b ∨ a) ∧ (¬d ∨ ¬a ∨ ¬b)
x2 := (b∨c → ¬a) = ¬b ∧ ¬c ∨ ¬a
x2dnf := (¬b ∧ ¬c) ∨ ¬a
x2cnf := (¬b ∨ ¬a) ∧ (¬c ∨ ¬a)

As I said, we might need the negations of these formulas. That would look like this:
notx1cnf = ¬x1dnf = (¬b ∨ d) ∧ (¬b ∨ a) ∧ (b ∨ ¬d ∨ ¬a)
notx1dnf = ¬x1cnf = (¬b ∧ ¬d) ∨ (¬b ∧ ¬a) ∨ (d ∧ a ∧ b)
notx2cnf = ¬x2dnf = (b ∨ c) ∧ a
notx2dnf = ¬x2cnf = (b ∧ a) ∨ (c ∧ a)

Now, the original formula is as easy as this:
x1 ↔ x2 ↔ a
We can now unfold DNF-style and continue from there:
x1 ↔ x2 ↔ a = (x1 ∧ (x2 ↔ a)) ∨ (¬x1 ∧ ¬(x2 ↔ a))

This is a conjunction of two bigger formulas. If the not-DNF/CNF formulas were disjunctions as well, that's already be a DNF. So how do we get the said inner not-DNF/CNF formulas to DNF? They are conjunctions of two formulas. If they x1 ∧ (x2 ↔ a)) and (¬x1 ∧ ¬(x2 ↔ a) were conjunctions of DNF, we'd just need the crossproduct of these DNF. Luckily, we already prepared DNF for x1 and ¬x1, so we just need to get (x2 ↔ a) and ¬(x2 ↔ a) = (¬x2 ↔ a) = (x2 ↔ ¬a)  to DNF.
(x1 ∧ (x2 ↔ a)) ∨ (¬x1 ∧ ¬(x2 ↔ a)) = (x1 ∧ ((x2 ∧ a) ∨ (¬x2 ∧ ¬a))) ∨ (¬x1 ∧ ((x2 ∧ ¬a) ∨ (¬x2 ∧ a))) =  (x1dnf ∧ ((x2dnf ∧ a) ∨ (notx2dnf ∧ ¬a))) ∨ (notx1dnf ∧ ((x2dnf ∧ ¬a) ∨ (notx2dnf ∧ a)))

Next, you need to get terms like (x2dnf ∧ a) to DNF. That's easy. Just take the DNF x2dnf and add a to every co-clause. Similarly for the three other similar subformulas. Once you have the DNF for these subformulas, disjunctions like (x2dnf ∧ a) ∨ (notx2dnf ∧ ¬a) tell you to unite them. Then there is just a conjunction with x1dnf left, which just means forming the crossproduct. And in the end, it's another disjunction of two DNF, which is again just a union.