> So this must there is some characteristic of the problems that we generate in practice that makes them "easy" but we don't have a good understanding of what t

> So this must there is some characteristic of the problems that we generate in practice that makes them "easy" but we don't have a good understanding of what this characteristic is. All we know, for now, is that we've somehow stumbled upon a near-perfect set of heuristics that work amazingly well on the SAT instances we encounter in practice. There's also the intriguing possibility that "natural instances" however one might define them arise through some complicated process that ends up sampling from easy SAT instances. I think of it as analogous to the Benford's law (see: https://en.wikipedia.org/wiki/Benford%27s_law#Explanations https://en.wikipedia.org/wiki/Benford%27s_law#Explanations) except that we do not have nearly as good explanations for SAT solvers. It is also highly likely that MOST instances of SAT are easy but that doesn't preclude it from being NP hard, nor does it stop us from easily constructing hard instances. (Such things are absolutely necessary for cryptography as an example.)