Computer Science Department
School of Computer Science, Carnegie Mellon University


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