Right. SAT solvers are an excellent theoretical fit and a terrible practical fit, at least at the current state of tooling. Their runtime _does_ explode and the tooling _is not_ any good at hinting as to why even when the explanation turns out to be very simple. "lol install takes an hour now" makes for a very poor error message, and debugging a black box that takes an hour to evaluate each input is just.... ugggggghh, and I can only thank my lucky stars that it did finish after an hour rather than taking an indefinite amount of time.

In contrast, the "danger" of heuristics is that they fail to dig up an exceedingly clever combination of archaic package versions that technically fit the user's specified requirements. It's such a small problem that it might even be considered a feature, since said exceedingly clever combinations are likely to be the result of poor version definitions and unlikely to be what the user actually wants.

Of course, if the only people who can be persuaded to write package managers are people doing research in the subject, then I suppose letting them inflict their pet projects on us is one way to compensate them for an otherwise thankless task, and perhaps in that sense it's fair.