5 ms·
Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.
by myng111 12d ago
Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.
- karelpeeters 12d 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.