It’s worth learning the basic use of some constraint solver, since they are now so fast and powerful. Z3 is free software and is very, very good, and you’d be surprised how many problems it can tackle (see: hundreds of examples in this book) that might actually come up in your work or life. In particular, you can attack scheduling problems with Z3 and people will think you are a wizard.
Those are small examples but you can scale them up and Z3 can still handle it.
I have no meaningful experience in OR, don’t know how SAT solvers work or how Z3 reduces things to SAT. Yet I was able to use it to attack a really gnarly scheduling problem with hundreds of variables, weird constraints, preferences, etc.
In addition to finding feasible solutions Z3 has an “Optimize” class that can handle soft constraints and objective functions. This is really useful. (I suspect CPLEX/Gurobi would be better at this but Z3 still works well.)
It’s worth learning the basic use of some constraint solver, since they are now so fast and powerful. Z3 is free software and is very, very good, and you’d be surprised how many problems it can tackle (see: hundreds of examples in this book) that might actually come up in your work or life. In particular, you can attack scheduling problems with Z3 and people will think you are a wizard.