Solving pseudo-Boolean problems with SCIP

Pseudo-Boolean problems generalize SAT problems by allowing linear constraints and a linear objective function. Different solvers, mainly having their roots in the SAT domain, have been proposed and compared, for instance, in Pseudo-Boolean evaluations. One can also formulate Pseudo-Boolean models as integer programming models. That is, Pseudo-Boolean problems lie on the border between the SAT domain and the integer programming field. In this paper, we approach Pseudo-Boolean problems from the integer programming side. We introduce the framework scip that implements constraint integer programming techniques. It integrates methods from constraint programming, integer programming, and SAT-solving: the so-lution of linear programming relaxations, propagation of linear as well as nonlinear constraints, and conflict analysis. We argue that this approach is suitable for Pseudo-Boolean instances containing general linear con-straints, while it is less efficient for pure SAT problems. We present extensive computational experiments on the test set used for the Pseudo-Boolean evaluation 2007. We show that our approach is very efficient for optimization instances and competitive for feasibility prob-lems. For the nonlinear parts, we also investigate the influence of linear programming relaxations and propagation methods on the performance. It turns out that both techniques are helpful for obtaining an efficient solution method