A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization
Peter M. Barth · MPG.PuRe (Max Planck Society) · 1995
The Davis-Putnam enumeration method (DP) recently evolved to one of the fastest known methods for solving the clausal satisfiability problem of propositional calculus. We present a generalization of the DP-procedure for linear pseudo-Boolean (or 0-1) inequalities and make use of the achievements for DP. We extend the method to optimize a linear pseudo-Boolean objective function w.r.t. a set of linear pseudoBoolean inequalities. The algorithm compares well with traditional linear programming based methods on a variety of standard 0-1 integer programming benchmarks.