Implement a translator that translates satisfiability instances
into equivallent 3-SAT instances.
(*)
Design and implement a backtracking algorithm to test whether
a set of formulae are satisfiable.
What criteria can you use to prune this search?
(*)
Implement the vertex cover to satisfiability reduction, and run
the resulting clauses through a satisfiability testing code.
Does this seem like a practical way to compute things?
