Concerning Question 1, there have mainly been two lines of work to find tractable restrictions of SAT.
The first one that you are already familiar with is to restrict the types of the clauses that you are allowed to use. For example, in 2-SAT, you are only allowed to use size two clauses. In Horn-SAT, you only allow Horn clauses etc. The tractable restrictions for SAT have been completely classified by Schaefer in 1978 [1] in his celebrated dichotomy Theorem. The result is a dichotomy in the sense that Schaefer showed that the restriction gives you either a problem in P or an NP-complete problem. It has later been generalized to the problem of counting the satisfying assignments [2] or to the problem of enumerating them [3].
Some of these restrictions indeed lead to better performances of SAT solvers. For example, on a 2-SAT instance, unit propagation will naturally solve the instance in polynomial time and one can observe a similar behavior for Horn clauses. However SAT solvers rarely try to detect if the input is of such a form as it would be too costly to scan all clauses (for hardcore SAT-solver people, linear time is already too slow ;)). So for example, affine formulas will often not be detected (CryptoMiniSat may be an exception here).
The second line of research is to look for tractable instances by trying to uncover some structure in the way the variables interact with the clauses. For example, given a CNF formula, you can look at its incidence graph: it is a bipartite graph whose vertices are the variables and the clauses of the formula and you have an edge between a clause $C$ and a variable $x$ if $x$ or $\neg x$ is in $C$. Now, if this graph is a tree, you can solve SAT in polynomial time by doing some dynamic programming on the tree.
Many results extend this observation and most of them are interested in the parametrized complexity of SAT. For example, a well-known parameter of graphs is the treewidth, an integer that intuitively measures how far a graph is from being a tree. Now, if the incidence graph from above has treewdith $k$, we know algorithms to solve SAT in time $2^{O(k)}\mathsf{size}(F)$, that is, a linear time algorithm if the treewidth is bounded. An early and good survey of these results have been written by Szeider in 2003 [4]. The earliest result of this kind for SAT I am aware of is a paper by Dantsin [5] where he apparently shows the tractability of SAT on bounded branch width graphs (the paper is in Russian and I have never read it but I trust Alekhnovich and Razborov [6] which improved the result in 2002). Many things have been understood since, for more general parameters and for more general problems (#SAT for example). I am shamelessly citing my thesis here as it contains a whole chapter reviewing most recent improvements on the question since then [8].
The idea of restricting the structure of the input through some associated graph has however been transpiring in computer science in many other domains as early as the 80's. See for example the Yannakakis algorithm for conjunctive queries in databases [7].
Now these tractable instances of SAT do not explain the good performances of SAT-solvers at all. Most of the algorithms used to solve these instances are not directly related to the way SAT-solvers work. But for more complex problem such as #SAT, the links between the theoretical algorithms and the way solvers work in practice is much stronger.
Some work has been done to understand the performances of SAT solvers by analyzing the structure of the formula (by detecting communities for example) but I do not know the literature well enough and let someone more competent than me answer this. All I can say is that it is not really related to the fact that the input belongs to some tractable instance. What you need is good heuristics to quickly converge to one solution. When there is no solution, then proof complexity is also a way of understanding the performances of a SAT-solver as it constructs a refutation of the formula while solving it. Thus, if no small refutation exists, then you can derive a lower bound on the runtime of the solver. But again, this is not completely enough to explain the performances of the SAT solver.
Concerning Question 2, I am not aware of any problem that have been discovered to be in P by reducting to a tractable class of SAT as usually, it is easier to program an algorithm than to encode it into a restricted formula. Moreover one generally prefers direct algorithms because they give more insights on the problem. However, a recent paper by Lampis, Mengel and Mitsou [9] shows the tractability of many parametrized problems by reducing them to SAT with bounded treewidth (which is known to be tractable). In this case, it is indeed usually simpler to writer the reduction instead of redoing complex dynamic programming algorithms again.
References
[1] Schaefer, Thomas J. (1978). "The Complexity of Satisfiability Problems". STOC 1978 https://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem
[2] Creignou, Nadia, and Miki Hermann. "Complexity of generalized satisfiability counting problems." Information and computation 125.1 (1996): 1-12.
[3] Creignou, Nadia, and J-J. Hébrard. "On generating all solutions of generalized satisfiability problems." RAIRO-Theoretical Informatics and Applications 31.6 (1997): 499-511.
[4] Szeider, Stefan. "On fixed-parameter tractable parameterizations of SAT." International Conference on Theory and Applications of Satisfiability Testing. Springer, Berlin, Heidelberg, 2003.
[5] E. Dantsin. Parameters defining the time of tautology recogni-
tion by the splitting method. Semiotics and information science, 12:8–17, 1979.
[6] Alekhnovich, Michael, and Alexander A. Razborov. "Satisfiability, branch-width and Tseitin tautologies." The 43rd Annual IEEE Symposium on Foundations of Computer Science, 2002. Proceedings.. IEEE, 2002.
[7] Yannakakis, Mihalis. "Algorithms for acyclic database schemes." VLDB. Vol. 81. 1981.
[8] Capelli, Florent. Structural restriction of CNF-formulas: application to model counting and knowledge compilation, Thèse de Doctorat, Université Paris-Diderot, 2016.
[9] Lampis, Michael, Stefan Mengel, and Valia Mitsou. "QBF as an Alternative to Courcelle’s Theorem." International Conference on Theory and Applications of Satisfiability Testing. Springer, Cham, 2018.
