|
|
|
|
|
by munificent
2890 days ago
|
|
> dep is, and always was, meant as an experiment to learn from. My impression is that the dep folks understand that too. The problem is that there is no consensus on what was learned from it. The dep folks seem to have come away convinced that a SAT-solver approach is the better approach. rsc is clearly convinced of the opposite. Everyone knows it is ultimately rsc's call, so I don't think talking about the power dynamics is very interesting. What I am more interested in is whether or not it's the right call. A good faith interpretation is that the dep folks aren't sad that their solution lost, it's that what they believe is a better solution lost. |
|
Satisfiability problems of this kind appear in a ridiculous number of fields and applications (and not just by reduction).
The vast majority of them, in practice, are approximated rather than exactly solved.
Most of the ones that are exactly solved are in software verification, model checking, etc. Areas where having an exact answer is very critical.
Outside of that, much like you see in MVS, they approximate or use heuristics. And it's fine. You don't notice or care.
The idea that "package management" is one of those areas that absolutely must be exactly solved to generate acceptable results seems to me to be ... probably wrong.
There are much more critical and harder things we've been approximating for years and everyone is just fine with it.
(IE not clamoring for faster exact solvers).
Thus i have trouble saying a sat solver is a better solution. It certainly would be a more "standard" one in this particular instance, but that's mostly irrelevant. It's also a very complex one that often fails in interesting ways in both this, and other, domains.