Hi,
Thanks for the fast reply.
The project I'm working on is far from being top secret since it is hosted at the eclipse foundation. In a few words, this project, equinox p2 [1,2], consists in replacing the eclipse update manager with something more flexible and robust. As part of this effort I have been investigating the usage of solvers (SAT and PB) mostly following what is described in the OPIUM paper [3].
I don't have yet at my disposal any of the large problems, but I know they could be that large because some eclipse distros are pretty large and the mapping we apply from our domain objects [4] to PB solvers is pretty verbose. When I get one of the large problem I will share it with you if you are interested.
> 1000 variables is ok but 40 000 constraints might be terrible for the PB solver.
Is this a general statement about PB solvers? What else could I use? Note that I've been using PB solvers simply because SAT solvers can't give me an optimal solution, and also I liked the "standard" input format that these solvers work on.
Thanks,
PaScaL
[1] <a href="http://www.eclipse.org/equinox/incubator/provisioning/" target="_new">http://www.eclipse.org/equinox/incubator/provisioning/</a>
[2] <a href="http://wiki.eclipse.org/Equinox_p2" target="_new">http://wiki.eclipse.org/Equinox_p2</a>
[3] <a href="http://www.cs.ucsd.edu/~lerner/papers/opium.html" target="_new">http://www.cs.ucsd.edu/~lerner/papers/opium.html</a>
[4] <a href="http://wiki.eclipse.org/Equinox_P2_Resolution" target="_new">http://wiki.eclipse.org/Equinox_P2_Resolution</a>
Start New Thread
