How to convert $((A\lor B)\land ((B\leftrightarrow A)\rightarrow C))\lor(C\rightarrow \lnot A)$ into CNF.

Question

I started off with:

$$((A\lor B)\land ((B\leftrightarrow A)\rightarrow C))\lor(C\rightarrow \lnot A)$$

And I've managed to get to:

$$((A\lor B) \land (((B\land \lnot A) \lor (A \land \lnot B)) \lor C)) \lor (\lnot C \lor \lnot A)$$

How do I finish and get this into CNF?

Answer 1

Hint: $\neg(A\leftrightarrow B)$ $\equiv (A\wedge\neg B)\vee(\neg A\wedge B)\\ \equiv (A\vee B)\wedge(\neg A\vee\neg B) $

Answer 2

Note that if $\lnot (A\wedge C)$, this expression is true, so we don't need to consider the other expression. Hence, we only need to consider the larger clause for the case that $(A\wedge C)$ is true.

Hence, $(A\vee B)$ is always true, so a true statement conjuncted with another statement is logically equivalent to that other statement.

So, so far we have

$$((B\land \lnot A) \lor (A \land \lnot B)) \lor C) \lor (\lnot C \lor \lnot A)$$

Next, note that under our assumption that $C$ is true, we know that the inner expression is a clause disjuncted into $C$, which means it is always true.

Hence, this expression can never be not true. The simplest CNF that could be made for this expression is $(C\vee\lnot C)$.