# Transform the formula for an arbitrary variable ordering into CNF:

+1 vote
```(((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

```

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

## 2 Answers

0 votes

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

by (25.6k points)
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.
0 votes

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```

by (166k points)
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.

0 votes
2 answers
0 votes
1 answer
0 votes
0 answers
0 votes
1 answer
0 votes
1 answer