I think it's mostly true that SAT-solvers are better because of decades of research/engineering on them. However there is some speculation that your observation

I think it's mostly true that SAT-solvers are better because of decades of research/engineering on them. However there is some speculation that your observation that "you typically lose a lot of structure" is actually sometimes a win, because by "flattening" a representation it might allow some distant implicit constraints to propagate. In planning, for example, that's one hypothesis for where Graphplan and SATplan (two 1990s systems) got their win from, vs. traditional symbolic planners. Similar to a question that comes up in compilers, about optimizing high-level vs. low-level representations. High-level representations give you more specific semantic information, but turning everything into a flattened mud of combinator logic or CPS or SSA might allow for some whole-program optimizations that propagate originally-distant constraints.