3 ms·
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 c
by dhash 7y ago
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 7y agoOh, 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.