[haiku-development] Re: What for does SAT solver needed for package management?
- From: Oliver Tappe <zooey@xxxxxxxxxxxxxxx>
- To: haiku-development@xxxxxxxxxxxxx
- Date: Mon, 18 Jun 2012 10:27:59 +0200
Hi,
On 2012-06-18 at 09:27:53 [+0200], X512 <danger_mail@xxxxxxx> wrote:
> From:
> https://www.haiku-os.org/community/forum/what_does_sat_solver_needed_package_management
>
> As I understand package resolution in Haiku will be implemented using
> this. Boolean satisfiability problem is a NP-complete task. So
> depedency resolution can't be solved in polynomial time. I really don't
> understand what for does it need.
>
> Package resolution can be implemented like shared object resolution.
> For example package A requires package B v1.6 and package C v4.3. If
> you install package A, system will check existness and correct version
> range for packages B and C. If all is OK then package will be installed
> successfully, if not, system can request user to download packages or
> automatically download it from repositiry. I don't see any boolean
> satisfiability problem or NP-complete tasks. Searching package by name
> is log(N), enumerating depedencies is M, total is M*log(N).
>
> Can everyone explain where am I wrong?
I can try ;-)
In your example above, you seem to assume that packages declare dependencies
on exact versions of other packages (package A requires package B in version
1.6). What should happen if package B v1.6.1 is the only one available? It
doesn't match v1.6, but it may (or may not) be compatible ...
In order to allow for that (and to increase the flexibility), Haiku's
packages don't declare dependencies on exact versions of other packages
(package A requires package B in version 1.6), but on abstract resolvables
(package A requires something providing B in a version compatible with ABI
1.6).
In order to find a solution for a specific dependency problem, the solver may
have to try several possibilities for each resolvable (as more than one
package may provide the resolvable in question). Implementing the required
decision-making and backtracking code "manually" (as done in apt, yum, smart
and most other package managers) turned out to be rather difficult and error
prone. As a result, traditional package solvers do a good job most of the
time, but now and then fail in an unexpected way. That is most visible when
the dependency problem isn't solvable: if that happens, the traditional
package managers tend to cough up some seemingly strange error message, which
at times isn't helpful at all about why exactly the solution failed.
In contrast, a SAT-solver can always tell you why it failed to find a
solution (unless it failed because of a timeout, which just indicates that
the problem is too complicated). Additionally, benchmarks done by the
openSUSE's zypper team have shown that using a SAT-solver for package
resolution yields much better resolution times than traditional solvers. From
my own experience, I can only second that: using zypper, resolution times
have become a non-entity and the diagnostic messages have improved a lot, too.
Hope that helps?
cheers,
Oliver
Other related posts:
