What are the practical benefits of using a SAT-solver? Is it faster? I haven't had any problems with the results of apt's algorithms, but maybe others have. When installing/upgrading stuff, the update step seems to be much slower than the other steps.
Package upgrades are an example of SAT (the satisfiability problem)[1]. Apt and yum don't recognize this result and instead use a bunch of ad hoc rules. These often fail, when they could succeed. SAT will always find the answer, eventually, if there is one.
Now the issue is that SAT is NP-complete, so it could run for a very long time before it finds a solution. But there are very good solvers which "most of the time" (meaning, basically always) find a solution in a short time. They are also open source projects[2].
There's been an existence proof (zypper) that using a standard SAT solver is possible, works, and is fast.
I understand what using a SAT-solver implies, but I haven't noticed apt failing often in practical terms. The heuristics used seem to work fine for me.
