A well known characteristic of $k$-SAT instances is the ratio of the number of clauses $m$ over the number of variables $n$, i.e., the quotient $\rho = m/n$. For every $k$, there is a threshold value $\alpha$ s.t.\ for $\rho \ll \alpha$, most instances are satisfiable, and for $\rho \gg \alpha$ most instances are unsatisfiable. There has been a lot of research done for problems where $\rho \ll \alpha$, and for problems with sufficiently small $\rho$, $k$-SAT becomes solvable in polynomial time. See, for instance, Dimitris Achlioptas's survey article from the Handbook of Satisfiability (PDF).
I am wondering if any work has been done in the other direction (where $\rho \gg \alpha$), e.g., if we can somehow transform the problem from CNF to DNF in this case to solve it quickly.
So, essentially, What is known regarding SAT where $\rho = m/n \gg \alpha$?