Added the beginnings of a 'watched literals' backtracking SAT solver.