exercise sheet 1 question 2.b: Transform the formula for an arbitrary variable ordering into DNF

Question

Transform the formula for an arbitrary variable ordering into DNF:

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

How can I solve this problem without truth table?

Answer 1

My favorite procedure is based on the Shannon decomposition that quickly reduces the formula in many cases. In this case, even a decomposition on variable c with further simplification steps will do:

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

If you wonder why I decomposed by variable c, the answer is that it looked as if that would lead to a quick solution. Here is another solution if you decompose first by a, which is not so good since it requires another decomposition later:

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

Bytheway, there is also a minimal DNF for this example which is simply

    a|c|d

But that was not required, and that is also another story which is not told here. Anyway, you see that for DNFs, there are many correct solutions.

Comments

how do we know on which variable to apply the decomposition?
does this solution work as well for CNF or only for DNF?

---

In the end, any variable order yields a correct solution.

This does work for DNF and CNF, as the SNF has both a CNF, and a DNF representation.

x ? ( Y : Z)
= (x → Y) & (¬x → Z) = (¬x | Y) & (x | Z) (CNF)
= (x & Y) | (¬x & Z) (DNF)

---

So, as Martin said, any variable ordering is correct, but of course, their choice will influence the final result and also the work that is to be done. Which one is best, it very hard to compute and to foresee, it is the variable ordering problem of BDDs, which is NP-complete. A good guess is however, the number of occurrences, and in particular, real occurrences, meaning those that remain after first simplifications.

---

I tried to solve this problem with the same procedure but I got totally lost!
Transform the formula for an arbitrary variable ordering into CNF:
((a|c|a|c<->(d|d)&c)->(c|b|b|a->!b|(d<->a)))
would you please help me?

---

What is your problem? Can you explain? Try first some simplifications, if you have doubts to have done that correctly, use a teaching tool to convince yourself that it is correct. Then, do case distinctions by the Shannon decomposition as shown above. Where do you got lost?

---

I already used the online tool. here I'm not able to upload the picture of my solution. so I create another question. Thanks

---

Here the SNF trick:

 ((a|c|a|c<->(d|d)&c)->(c|b|b|a->!b|(d<->a)))
= c => ( ((true<->(d|d)&true)->(true|b|b|a->!b|(d<->a))) | ((a|false|a|false<->(d|d)&false)->(false|b|b|a->!b|(d<->a))))
= c => ( d->(!b|(d<->a)) | ((a<->false)->(b|a->!b|(d<->a))))
= c => ( d->(!b|(d<->a)) | (¬a → (b|a->!b|(d<->a))))
…
And so on. Decompose by a variable, simplify.
…
c => ( d ? ((¬b|a) : 1)  | d?((¬a → (b|a → ¬b|a)):(¬a → (b|a → ¬b|¬a))) )
…

Answer 2

Your formula is:
((c|c&a → ¬(b|c)) → (d|d|¬d)&(c|a|d))
There are some simplifications we can do:

• c|c&a = c (if we want to satisfy c&a, we already satisfied c, so c&a is redundant)
• (d|d|¬d) = 1 (we can drop this tautology)

((c → ¬(b|c)) → (c|a|d))

One more thing: c → ¬(b|c) = c → ¬b & ¬c. For c=1, this can't be satisfied. For c=0, this is satisfied independently of b. Hence, c → ¬(b|c) = ¬c. This argument is basically a Shanon decomposition by the variable c as @KS suggested.

((¬c → (c|a|d)) = ¬¬c | c | a | d

= c | a | d