[dhash]

SAT/SMT hardness regression has come a long way, especially if you can insert profiling information for real instances.

If this is a production model for the cloud, the engineer should have put some thought into the encoding as to express sat/unsat clearly, if possible.

In the general case, sure, to some extent one can construct an adversarial example just as with NN (random 3-sat hardness cliff). Real world formulations of problems are either nice or atrocious IME, discoverable at dev time.

[pron]

Oh, I don't mind adversarial examples. As a user of SMT solvers (for semi-automated program verification), I just find them unpredictable and frustrating. But I've never employed SMT solvers as a library in some production system, and it's good to hear that in that case the instances could be controlled well enough for the normal operation to be predictable.