We consider the satisfiability problem for Boolean combinations of generalized 2SAT constraints, which are linear constraints with at most two, possibly unbounded, integer variables having coefficients in {-1, 1}. We prove that if a satisfying solution exists, then there is a solution with each variable taking values in [-n \cdot (\bmax + 1), \; n \cdot (\bmax + 1)], where n is the number of variables, and \bmax is the maximum over the absolute values of constants appearing in the constraints. This solution bound improves over previously obtained bounds by an exponential factor. Our result enables a new enumerative approach to satisfiability checking. An experimental evaluation demonstrates the efficiency of this approach over previous techniques. As a corollary of our main result, we obtain a polynomial-time algorithm for approximating optima of generalized 2SAT integer programs to within an additive factor.

19 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu