Transform the formula for an arbitrary variable ordering into CNF:

Question

(((a->d)->!a)|(d&c->(a<->b)))&c
I don't know if I'm in the right direction. 
The problem is that I don't know exactly 
where I'm going and what to get in the end. 
Could someone help me? Thank you in advance

 

Comments

Please add the tag vrs (or dira if it is related to that lecture).

Answer 1

Looks quite good. So far, I spotted no mistake other than a missing parenthesis in the last line.

Next, I'd transform (a & ¬d) | ¬a | ¬d | ¬c. Since satisfying a&¬d already satisfies ¬d, we can drop a&¬d.

Then we are left with:
((¬a | ¬d | ¬c) | ((¬a | b) & (¬b | a))) & c // we then multiply out
=(¬a | b | ¬a | ¬d | ¬c) & (¬b | a | ¬a | ¬d | ¬c) & c // the clause in the middle is a tautology as there's a|¬a, the clause on the left has a redundant literal ¬a
=(¬a | b | ¬d | ¬c) & c // as the outer conjunction requires c to be satisfied, we can drop ¬c from the other clause
= (¬a | b | ¬d) & c

Comments

Thank you. Just that I don't understand the notion of satisfaction, redundancy and tautology that you used to reduce variables.

---

Satisfaction: A satisfying assignment of is a variable assignment that makes the formula rue.

Redundancy: Same thing twice.

Tautology: True for every assignment.

Answer 2

My favorite way to solve these kinds of questions is to use the Shannon decomposition:

    phi = a&phi[a<-true] | !a&phi[a<-false]          for DNF
    phi = (!a|phi[a<-true]) & (a|phi[a<-false])      for CNF

which works here as follows

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

Comments

Thank you. This is a very good and simple method. But from the decomposition with !c, I do not understand the next 4 lines.

---

After the decomposition by c, we got

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

where the second conjunct simplifies to c since phi&false becomes false and c|false is then simply c.

Then, we continue with a Shannon decomposition on variable "a" of the first conjunct, and simplify again to eliminate the constants true and false.