Are there any algorithms for SAT solving which are not DPLL based? Or are all algorithms used by SAT solvers are DPLL based?
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 & 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.
Survey propagation is another algorithm that has been used with success on some kinds of SAT problems, notably random SAT instances. Like WalkSAT, it cannot be used to prove unsatisfiability, but it is based on very different ideas (message-passing algorithms) from WalkSAT.
There are SAT solvers based on the local search. See, for example, this paper for exposition.
You can also say, that all CSP solvers are also SAT solvers. And there are as far as I know two methods used in CSP:
- Exhaustive DFS with prunning of the search space and checking arc consistency, possibly using shaving to ensure that consistency is maintained as soon as possible.
- Local methods (taboo search, simulated annealing)
Monte Carlo Tree Search (MCTS) has recently achieved some impressive results on games such as Go. The rough basic idea is interleaving random simulation with tree search. It is lightweight and easy to implement, the research hub page I linked contains many examples, papers and some code as well.
Previti et al.  did some preliminary investigation of MCTS applied to SAT. They call the MCTS-based search algorithm UCTSAT ("upper confidence bounds applied to trees SAT", if you will). They compared the performance of DPLL and UCTSAT on instances from the SATLIB repository, with the goal of seeing if UCTSAT would produce significantly smaller search trees than DPLL.
For uniform random 3-SAT and flat-graph coloring instances of different sizes, there were no significant differences. However, UCTSAT performed better for real-world instances. Average tree sizes (in terms of the number of nodes) for four different SSA circuit fault analysis instances were in several thousands for DPLL, while always less than 200 for UCTSAT.
 Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf, and Bart Selman. "Monte-carlo style UCT search for boolean satisfiability." In AI* IA 2011: Artificial Intelligence Around Man and Beyond, pp. 177-188. Springer Berlin Heidelberg, 2011.
DPLL does not strictly specify the variable-visit ordering and there is a lot of interesting research looking at optimal variable ordering attack strategies. some of this is incorporated into variable selection logic in SAT algorithms. in a sense some of this research is preliminary in that it shows that different variable attack orderings lead to different sequential constrainedness (which is highly correlated with instance hardness), and devising the most effective heuristics or strategies to exploit this apparently key insight seems to be in the early stages of research.