Replace resolver with constraint optimisation library

[leth]

I'm by no means an expert in these areas, but the problem which the resolver attacks seems to be a classic CS 'constraint optimisation problem'.

You have a set of variables (gem versions) and constraints (foo_version > 1.0), and you wish to maximize the sum of the gem versions (pick the highest conforming version of each gem).

The challenge of solving these problems these might be better served by a specialist library.

Of course, adding an external dependency may not be an option for you (I note that bundler currently has none), but the information my be helpful to someone (sorry if you've heard it before).

[gnufied]

Thank you for reporting this. We are/were looking into SAT solvers for same purpose and currently evaluating bunch of options. We already have quite a bit of resolvers tickets open, so I will close this one because it is not really bug/issue.

[leth]

No problem! I mostly filed this in case the information would be of use to anyone.

Be careful how you approach this; a boolean satisfiability problem is subtly different to a constraint optimisation problem.
Solving a boolean satisfiability problem will find you an acceptable set of gem versions, but it will not try to maximise the versions, so you will get ANY solution rather than the one with the highest versions.

[aspiers]

We already have quite a bit of resolvers tickets open

It would have been helpful to provide links to those ;-)

[aspiers]

After a quick glance/search I failed to find any obvious status on work to improve the resolver, so I'm not sure what the latest is, although AFAICS lib/bundler/resolver.rb is not yet using a SAT solver. If you guys are still looking into SAT solvers (and I hope you are, because it works awesomely for zypper ;-) then maybe you will find https://github.com/openSUSE/sat-solver-bindings useful. Probably you already know about it but I just wanted to make sure ;-) Hope that helps!

[Who828]

@aspiers Well all the resolver bugs have been fixed as of 1.6 of Bundler. We rewrote the resolver in pure Ruby to maintain compatibility with all flavors of Ruby and we were adamant of not having any external dependencies. While its not the fastest resolver out there, its much better then our old one and serves our needs for now.

While the sat-solver looks really nice, I am a huge fan of Gecode (http://www.gecode.org/) it has to be the best CSP solving library I have seen so far. The performance is top notch and supports lot of ways of about resolving dependencies. It also has ruby bindings like the SAT solver.

Though the SAT solver source code can be useful place to gain new ideas on improving our own resolver when we hit a bottleneck again :)

[aspiers]

Thanks very much for the info! But I'm not yet convinced by the statement that "all the resolver bugs have been fixed as of 1.6 of Bundler" - please see #2965 which I just filed.

[skottler]

@aspiers yeah, that's not a bug in the resolver, but rather a feature request.