A couple of months ago I tried using z3 to create an itinerary for my honeymoon. It seemed like a very straightforward implementation of a TSP with a few extra restrictions. It's 2024 and I had an M2 - which is basically alien tech for the period when these problems started being solved - so I figured that in 5 minutes' time I'd have the perfect walking trip in Rome. To quote TFA, how hard could it be?

The whole story might become a blog post some day, but the punchline is that Moore's law ain't got nothing on NP-hard problems