First step, you abbreviate all subformulas with new variable names:
- x0 <-> c & d
- x1 <-> !x0
- x2 <-> b | x1
- x3 <-> a -> b
The true meaning of this is that the given formula is equivalent to the following quantified formula
∃x0 x1 x2 x3.
(x0 <-> c & d) &
(x1 <-> !x0) &
(x2 <-> b | x1) &
(x3 <-> a -> b)
So, when we are interested in the satisfiablily of the original formula, then it is satisfiable if and only if the above quantified formula is satisfiable, and that is the case if and only if the following is satisfiable:
(x0 <-> c & d) &
(x1 <-> !x0) &
(x2 <-> b | x1) &
(x3 <-> a -> b)
The next step is to replace these equivalences with their conjunctive normal forms. You can do that in that you compute the CNF for each one, but since there is one pattern for each operator, you may prepare that also on your notes. You will find those for negation, conjunction and disjunction on slide 113 of the propositional logic chapter.
That's all. Why doing that? Since modern SAT solvers work on conjuncitve normal forms, and the problem is that in general, a conjunctive normal form may have an exponential size in terms of the length of the given formula. The above equisatisfiable clause form is having a linear size, and is sufficient for SAT checking.
