SAT algorithms not based on DPLL
Resolution Search (just applying the resolution rule with some good heuristics) is another possible strategy for SAT solvers. Theoretically it's exponentially more powerful (i.e. there exist problems for which it has exponential shorter proofs) than DPLL (which just does tree resolution though you can augment it with nogood learning to increase its power - whether that makes it as powerful as general resolution is still open as far as I know) but I don't know of an actual implementation that performs better.

If you don't limit yourself to complete search, then WalkSat is a local search solver which can be used to find satisfiable solutions and outperforms DPLL-based search in many cases. One can't use it to prove unsatisfiability though unless one caches all the assignments that have failed which would mean exponential memory requirements.

Edit: Forgot to add - Cutting planes can also be used (by reducing SAT to an integer program). In particular Gomory cuts suffice to solve any integer program to optimality. Again in the worst case, an exponential number may be needed. I think Arora &amp; Barak's Computational Complexity book has a few more examples of proof systems that one could in theory use for something like SAT solving. Again, I haven't really seen a fast implementation of anything apart from DPLL-based or local search based methods.