A first shot at solving satisfaction: convert to Disjunctive Normal Form (DNF).
What is DNF?
How do we check satisfiability of a formula in DNF?
Why is this not an acceptable solution?
