An implementation of the DPLL algorithm