CMU-CS-04-179 Computer Science Department School of Computer Science, Carnegie Mellon University CMU-CS-04-179 On Solving Boolean Combinations of Generalized 2SAT Constraints Sanjit A. Seshia, K. Subramani, Randal E. Bryant November 2004 Keywords: Generalized 2SAT constraints, unit two variable per inequality constraints, Boolean satisfiability, automated theorem proving, integer linear programming, decision procedures, constraint satisfaction, verification, optimization 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