SAT solver optimizations of DPLL for unsatisfiable formulas
Conflict analysis and clause learning and non-chronological backtracking should help a lot, for both satisfiable and unsatisfiable instances.  They discover large portions of the search space where no solution can reside and prune the search to avoid traversing those.

You could also try two-watched-literals unit propagation, but I'd try the others first, as I expect they'll make a bigger difference.