Resolver and inefficiencies

[Pascal Rapicault]

Hi 

My name is Pascal Rapicault. I'm the maintainer of the Eclipse p2 resolver (the dependency resolver used by Eclipse install mechanism). 
Rather than implementing a resolver from scratch, since the dependency problem is NP complete (I assume the jigsaw also is), we have been using a SAT solver (http://www.sat4j.org) and have been quite happy with it. It is very efficient and scales very well.

If this can be helpful, maybe we could find a way to share knowledge on this.

Sincerely, 

Pascal
=-=-=
Consulting, training, bug fixing


On 2012-05-03, at 11:13 AM, Paul Sandoz wrote:

> Hi,
> 
> This observation may already be known, but i thought i would throw this out here anyway...
> 
> When the following modules are installed into a library:
> 
>  module a @ 1.0 {
>    requires c @ <= 1.1;
>    requires b;
> 
>    class a.A;
>  }
> 
>  module b @ 1.0 {
>    requires c @ 1.0;
> 
>    class b.B;
>  }
> 
>  module c @ 1.0 { }
> 
>  module c @ 1.1 { }
> 
> it results in a heck of a lot of searching through the dependency graph (note that the jdk.base dependency is synthesized so there is more going on than shown above).
> 
> Module a at 1.0 will initially select c at 1.1, but module b at 1.0 requires c at 1.0 so the resolution algorithm will backtrack and eventually try a at 1.0 with c at 1.0.
> 
> Due to the way the resolver is implemented using the call stack this backtracking is very inefficient when there are optional dependencies. Sub-graphs are re-evaluated multiple times until the call stack eventually unwinds to try a at 1.0 with c at 1.0.
> 
> One solution is have the error propagate in the return value so the call stack knows whether it should keep unwinding i.e. for conflict with module c it should unwind to the point where the decision to select c at 1.1 was made so c at 1.0 and it's dependencies can be searched.
> 
> Something tells me this is still not particular efficient and there is probably a better way...
> 
> Paul.