6 ms·
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?
by thisisauserid 13d ago
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?
- myng111 13d agoZ3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.
- karelpeeters 13d agoIn 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.
- nostrebored 13d agoz3 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.