alt Hacker NewsI know nothing about z3 but it's from Microsoft. Would Google's OR-Tools component CP-SAT also be useful for something like this?
Replies
myng111 • today at 3:15 PM
Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.
➕ show 1 reply
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.