Cpp Recursive DPLL