Resolver and inefficiencies

[mark.reinhold at oracle.com]

2012/5/3 14:03 -0700, pascal at rapicault.net:
> 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.

Hi Pascal, nice to meet you.

It'd be great if we could learn more about how p2 uses Sat4j.  I've been
thinking for a while now that we should explore this option for Jigsaw.
Even if our resolution problem winds up not being NP-hard, a good SAT
solver can likely be more efficient than the simpleminded backtracking
algorithm we use now.

I found http://wiki.eclipse.org/Equinox_P2_Resolution -- is that the
best overview document?

- Mark