
CMUCS04179
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS04179
On Solving Boolean Combinations of Generalized 2SAT Constraints
Sanjit A. Seshia, K. Subramani, Randal E. Bryant
November 2004
CMUCS04179.ps
CMUCS04179.pdf
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 polynomialtime algorithm for approximating optima of generalized 2SAT
integer programs to within an additive factor.
19 pages
