DPLL (for real!) Davis – Putnam – Loveland – Logemann dpll(F, literal){ remove clauses containing literal shorten clauses containing  literal if (F contains no clauses)return true; if (F contains a unit or pure L) return dpll(F, L); choose P in F; if (dpll(F,  P))return true; return dpll_2(F, P); } Where could we use an heuristic to further improve performance
{}