An implementation of an OSGi resolver is a complex beast. Just ask Tom Watson, the Equinox dev lead :-) The Equinox p2 project, a new provisioning system for Eclipse, also has similar and complex resolve algorithm. Recently the p2 project, changed to use the SAT4J SAT solver to drive their resolve algorithm.
We have proposed a Google Summer of Code project for someone to investigate replacing the current Equinox runtime resolver with SAT4J (or another suitable constraint solver). So if this project sounds interesting to you, please sign up for it!