SAT solver optimizations of DPLL for unsatisfiable formulas I am implementing a SAT solver based on DPLL algorithm, and it works fine on small formulas and larger satisfiable problems. My case split is based on a tree like structure, where every branch is tried one by one until solution for the problem is found or until every branch is tried. 

So my problem now is that the above described approach does not terminate when trying to find a solution on large UN-SAT problems (so there shouldn't be a solution), therefore my program tries every possibility $2^n$, giving it a run time of years to solve UN-SAT problem with $50$+ variables (it would eventually terminate in years as I am not having any memory issues etc.).

My question is: what topics/implementations would I want to look at to speed up the tree processing or this case split process on unsatisfiable problems. Thanks.
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.