\item \self Consider the problem of deciding satisfiability of quantifier-free theory formulas. What are the main advantages of the DPLL(T) algorithm over eager encoding and lazy encoding?
