Building Efficient Decision Procedures on top of SAT solvers