[microarchitect]

Although SAT is indeed NP-complete, modern solvers are ridiculously fast for the kinds of SAT queries that appear in scenarios like hardware model checking and verification. It's not uncommon for queries with millions of variables and clauses to be solved in a matter of seconds. There are some algorithmic tricks combined with clever data structures and search space exploration heuristics that make this possible.

btw, if you're curious about the workings of a modern SAT solver, the first few sections of this paper: http://www.georg.weissenbacher.name/papers/mod12.pdf should make interesting and hopefully accessible reading.

Unfortunately, I don't know enough about the internals of Z3 to know what specifically makes it the fastest SMT solver. But I also don't think it's too far wrong to say that SMT solvers like Z3 are fast because the underlying SAT solver they use is very fast.