By: Pascal Rapicault (pascal)|
Date: 2007-11-14 15:08
Subject: RE: Pseudo boolean solver
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 .
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  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.