I am typing this quite quickly due to severe time constraints (and didn't even get to responding earlier for the same reason), but I thought I would try to at least chip in with my two cents.
I think this is a truly great question, and have spent a nontrivial amount of time over the last few years looking into this. (Full disclosure: I have received a big part of my current funding precisely in order to try to find answers to questions of this type, and then potentially to convert deeper insights into SAT into more efficient SAT solvers.)
If one would have to give a one-sentence answer, then I think
nobody really knows and this is an active area of research
is pretty much as good as it gets. Except that that there is a lot more room for more activity, especially from the theory side.
Some proposed explanations (not mutually exclusive), which have already been discussed in other answers and comments, are
- (a) backdoors,
- (b) parameterized complexity considerations,
- (c) graph structure of the CNF problem,
- (d) proof complexity considerations, and
- (e) phase transitions.
Starting from the end (e), there seems to be quite some confusion regarding phase transitions. The short answer here is that there is no reason whatsoever to believe that the ratio of clauses to variables is relevant for applied problems or theoretical combinatorial problems (a.k.a. crafted instances). But for some reason it is a not too uncommon misconception in the applied part of the SAT community that the clauses-to-variables ratio should somehow be a generally relevant measure. The clause-to-variable ratio is very relevant for random k-SAT, but not for other models.
My feeling is that backdoors (a) have been a popular explanation, but I personally have not really seen convincing evidence that it explains what goes on in practice.
Parameterized complexity (b) provides a beautiful theory about some aspects of SAT, and a very attractive hypothesis is that SAT instances are easy because they tend to be "close to some island of tractability." I think this hypothesis opens up many exciting directions of research. As noted in some of the answers, there are a lot of connections between (a) and (b). However, so far I don't really see any evidence that parameterized complexity correlates too much with what is going on in practice. In particular, it seems that instances that are tractable can be very, very hard in practice, and instances without any small backdoors can still be very easy.
The explanation that seems most believable to me for industrial instances is (c), namely that the (graph) structure of the CNF formulas in question should be correlated with practical SAT performance. The idea here is that variable and clauses of industrial instances can be clustered into well-connected communities with few connections between, and that SAT solvers somehow exploit this structure. Unfortunately, it seems quite hard to pin this down more rigourously, and equally unfortunately this area suffers from a fair amount of hype. The proposed explanations I have seen so far in papers are quite unsatisfactory and the models seem to be easy to shoot down. The problem would seem to be that if one really wants to do this thoroughly, then the math gets really hard (because it is a hard problem) and it also gets extremely messy (because you need your model to be close enough to reality to get relevant results). In particular, the papers I have seen explaining that the performance of the VSIDS (variable state independent decaying sum) heuristic for variable choices works well because it explores communities in the graph representation of the instances are quite unconvincing, although the hypothesis as such is still very attractive.
One line of research that I have personally pursued is whether practical SAT performance somehow correlates with proof complexity measures of the CNF formulas in question. Unfortunately, the short answer seems to be that there really is no clear and compelling connection. It might still be that there are nontrivial correlations (this is something that we are currently investigating in different ways), but it seems theory is too nice and clean and pretty and reality is too messy for there to be a really good match. (Regarding the paper Relating Proof Complexity Measures and Practical Hardness of SAT by Järvisalo, Matsliah, Nordström, and Živný in CP '12 it has turned out that more detailed experiments provide a much more complex picture with less clear conclusions --- we hope to get to a full journal version reporting on this any decade now, but it is complicated, though still hopefully interesting.)
Another, related, line of work in proof complexity is to model state-of-the-art SAT solvers as proof systems and prove theorems in these models to deduce properties of the corresponding solvers. This is a bit of a minefield, though, in that small and seemingly innocuous design choices on the theoretical model side can lead to the results being pretty much completely irrelevant from a practical point of view. On the other hand, if one wants a theoretical model that is close enough to reality to give relevant results, then this model gets extremely messy. (This is because SAT solver performance depends on the global history of everything that has happened so far in nontrivial ways, and this means the model cannot be modular in the way we usually set up our proof systems --- whether a particular derivation step is "correct" at a certain point in time cannot be locally verified, but depends on the whole proof so far.)
Two papers that really should be mentioned as exceptions to this, though, are [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte and Thurley 2011], where it is shown that conflict-driven clause learning SAT solvers modelled in a natural way have the potential to polynomially simulate full, general resolution. There are a fairly long list of papers preceding [PD11] and [AFT11] that essentially claim the same result, but they all have serious issues with the modelling. (It is true that [PD11] and [AFT11] also need some assumptions to work, but they are pretty much the minimal ones you would expect unless you are asking for papers that would also show that the parameterized complexity hierarchy collapses.)
Again, I am writing all of this very quickly, but if there is substantial interest for anything of the above I could try to elaborate (although it might take a while to return to this again --- please feel free to ping me if there is anything you would want me to comment on). As a quick way of providing references, let me do some shameless self-plugs (although the shame is decreased somewhat when I see that some comments have also cited some of these references):
Tutorial-style talk On the Interplay Between Proof Complexity and SAT Solving given at the International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning in 2016 with lots of full references at the end of the slides: http://www.csc.kth.se/~jakobn/research/TalkInterplaySummerSchool2016.pdf
Slightly more recent, and briefer, survey talk Understanding Conflict-Driven SAT Solving Through the Lens of Proof Complexity from early 2017 (also with full references at the end): http://www.csc.kth.se/~jakobn/research/TalkProofComplexityLensCDCL1702.pdf
Survey of connections between proof complexity and SAT solving: http://www.csc.kth.se/~jakobn/research/InterplayProofCplxSAT.pdf [Bibliographic reference: Jakob Nordström. On the Interplay Between Proof Complexity and SAT Solving. ACM SIGLOG News, volume 2, number 3, pages 19-44, July 2015. (Lightly edited version with some typos fixed.)]
SAT '16 paper with CDCL modelled faithfully as a proof system: http://www.csc.kth.se/~jakobn/research/Trade-offsTimeMemoryModelCDCL_SAT.pdf [Bibliographic reference: Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordström, and Marc Vinyals. Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT '16), Lecture Notes in Computer Science, volume 9710, pages 160-176, July 2016.]