3 ms·

> I've long wanted to integrate this type of solver into my workflow more, because I think that if I can make it into more of a habit, it would provide insane l

> I've long wanted to integrate this type of solver into my workflow more, because I think that if I can make it into more of a habit, it would provide insane leverage for prototyping. Does anyone have experience using these techniques for that? In my experience (and I'd love alternate viewpoints here, just because I want to use solvers more!), there are a limited set of areas where SAT, SMT, and MILP solvers are a reasonable choice, but in these situations they really shine. Any time you need to model and reason about something in terms of rules and constraints (business logic validation perhaps, schedules, layout engines, etc) solvers will help you cleanly solve the problem. Of course, then there's the additional problem that large models take large amounts of time to converge, so large problems may require more creative approaches. I've used MILP solvers in the past to determine optimal (given a model) average thread pool sizes, and average batch job wait times as well, but usually operating conditions change so frequently that models often provide poor performance. One of my favorite uses of Z3 though is ZetZ[1] a language that adds a verification layer atop C.

kqr 6y ago
You're probably not wrong, because what you're saying seems to be conventional wisdom. However, there's a part of me that can't help thinking, "...but that's only because we're not used to thinking of our problems in terms of rules and constraints. If we got into the habit of doing it, we'd soon find out that more and more of our problems are of the rules-and-constraints kind, if only looked at the right way." There's also an argument that you can turn any problem into rules and constraints, but doing so might not help you. I'm taking the stance here that maybe for a larger class of problems than we think it is actually helpful to think of them as rules and constraints. And then it's a small step to apply a generic solver as the first, baseline approach. So my argument is not really that "we should apply solvers wherever they are currently immediately obviously useful" but more that "there might be a high-potential paradigm shift hidden here where we as a profession can adapt a new way of thinking based on off-the-shelf solvers for generic problems, if only we learn to view the world that way, and this might turn out to be a better way to think of the lower level components of software engineering."

kqr 6y ago

You're probably not wrong, because what you're saying seems to be conventional wisdom. However, there's a part of me that can't help thinking, "...but that's only because we're not used to thinking of our problems in terms of rules and constraints. If we got into the habit of doing it, we'd soon find out that more and more of our problems are of the rules-and-constraints kind, if only looked at the right way." There's also an argument that you can turn any problem into rules and constraints, but doing so might not help you. I'm taking the stance here that maybe for a larger class of problems than we think it is actually helpful to think of them as rules and constraints. And then it's a small step to apply a generic solver as the first, baseline approach. So my argument is not really that "we should apply solvers wherever they are currently immediately obviously useful" but more that "there might be a high-potential paradigm shift hidden here where we as a profession can adapt a new way of thinking based on off-the-shelf solvers for generic problems, if only we learn to view the world that way, and this might turn out to be a better way to think of the lower level components of software engineering."