z3 is also just so thoroughly optimized that even if your formulation of the constraints is inefficient it is faster. it is a great library that lets you solve pretty complicated DP problems with a few dozen lines of code.
Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.
In general that's true, but to reason about boolean circuits like in this challenge we only need a SAT solver. Z3 is just used for it's convenient API.