|
|
|
|
|
|
by ritter2a
1875 days ago
|
|
|
I would say that the benefits you get from a habit of using SMT solvers depends a lot on the kind of problems you are working on. If your problem is rather small and self-contained, you can really win a lot with these solvers. E.g. I used an ILP solver to fairly distribute tasks to a group of people based on a heuristic of familiarity between each person and the tasks. That's only a few constraints in the solver that saved me a lot of manual or suboptimal coding work. Similarly, it was easy enough to quickly check whether two graphs satisfy a custom condition that is close to (but not quite) isomorphism that I wanted to give a try. If you are thinking of bigger, more complex tasks, the efficiency gains you get might vary more. If your problem produces many large solver queries, the chances are good that you will wait a long time for results. Without much practice, adjusting/augmenting your specification (and specifically in the case of ILP solvers: tuning the solver parameters) to reduce your solving times is a very non-trivial task. Either way, the solver probably won't bring you to 80% of the execution speed of a custom solution: I once sped up a task by 100-200x by replacing a Gurobi LP with a dumb, theoretically exponential, but easy to optimize custom implementation (the solver was however helpful for testing that the implementation was correct). Lastly, in my experience, once a constraint system/model reaches a certain complexity, it is a lot more difficult to debug than code in a programming language. There are useful techniques and tricks for debugging solver models, but the tooling and the sequential execution of real code make debugging of traditional code less of a head ache. |
|
|
Tailored implementations are great for problems that you have to solve frequently with no changes to the structure. In reality, requirements frequently change breaking many of previously valid assumptions for efficiently filtering the feasible space.