> I ended up using a tool called ‘z3’. It’s kind of magical? Every time it finds a solution I get a surge of joy.

This resonates so much. I had a similar feeling after going to my very first operations research lecture. Solving seemingly incomprehensibly complex problems by framing them as a bunch of simple constraints and getting a solution seemed like such magic.