Earlier quoted context omitted.
> SAT is pretty much a solved problem We don’t really understand what makes some SAT problems harder than others. You can go from a problem solvable with CDCL in a few seconds to one that would outlast the solar system by changing a couple of input bits.
Sure, but in practice that’s not what people worry about, from what I have seen. At least when dealing with SMT problems, the SAT part is the easy part.
It's sort of like how "in practice" it didn't matter for thousands of years that nobody understood electricity. Any problem that came up that would have required that knowledge to solve just got dropped, because they didn't have the tools to solve it.