Refactor DPLL into Solver

This simplies the hierachy in sat package. This also
introduce a timeout natively in the solver. It checks
the time at every top level loop iteration, which should
be good enough granualarity.

This also removed the barbarian timeout with scheduler
that was used to more esaily run historical benchmarking.