Are SAT solvers polynomial on practical instances?

Boolean satisfiability is the canonical NP-complete problem, so worst cases require exponential time unless P = NP. Yet modern CDCL solvers routinely solve instances with millions of variables. Why?

There is no theory that explains the gap between the worst-case complexity and the empirical behaviour of state-of-the-art solvers on industrial benchmarks. A useful characterisation of 'easy' SAT instances is an open problem.