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.
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.
Comments
I know nothing about z3 but it's from Microsoft. Would Google's OR-Tools component CP-SAT also be useful for something like this?
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.