I ask Claude to solve problems of similar complexity on a daily basis. A SAT solver specifically is maybe a once a week thing.

Use cases are anything, really. Determine resource allocation for a large project, or do Monte Carlo simulation of various financial and risk models. Looking at a problem that has a bunch of solutions with various trade-offs, pick the best strategy given various input constraints.

There are specialized tools out there that you can pay an arm and a leg for a license to do this, or you can have Claude one-off a project that gets the same result for $0.50 of AI credits. We live in an age of unprecedented intelligence abundance, and people are not used to this. I can have Claude implement something that would take a team of engineers months or years to do, and use it once then throw it away.

I say Claude specifically because in my experience none of the other models are really able to handle tasks like this.

Edit: an example prompt I put here: https://news.ycombinator.com/item?id=43639320