I'm a big fan of the CP-SAT solver. It was a remarkable piece of tech to learn about (especially Peter Stuckey's talks on lazy clause generation [1]).

I'd used it in a past life to build a Kubernetes scheduler [2] and tackle some cluster management problems.

[1] https://www.youtube.com/watch?v=lxiCHRFNgno [2] https://www.usenix.org/system/files/osdi20-suresh.pdf