What for does SAT solver needed for 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?