"Terse Integer Linear Programs for Boolean Optimization"
Article by Christoph Buchheim, Giovanni Rinaldi, available as BibTeX Source.
Zentrum für Angewandte Informatik Köln, Lehrstuhl Jünger
Preprint Key:	zaik2007-558
Keywords:	logic optimization, maximum satisfiability, pseudo-boolean optimization
MSC codes:	03B70, 65K05, 90C57
This article is to appear in "Journal on Satisfiability, Boolean Modeling and Computation".
Abstract:	We present a new polyhedral approach to nonlinear boolean optimization problems. Compared to other methods, our approach produces much smaller integer programming models, making it more efficient from a practical point of view. We mainly obtain this by two different ideas: first, we do not require the objective function to be in any normal form. The transformation into a normal form usually leads to the introduction of many additional variables or constraints. Second, we reduce the problem to the degree-two case in a very efficient way, using a slightly extended formulation. The resulting model turns out to be closely related to the maximum cut problem; we show that the corresponding polytope is a face of a suitable cut polytope in most cases. In particular, our separation problem reduces to the one for the maximum cut problem. In practice, our approach turns out to be very competitive. First experimental results, which have been obtained for some particularly hard instances of the Max-SAT Evaluation 2007, show that our very general implementation can outperform even special-purpose SAT solvers.