On solving Boolean combinations of UTVPI constraints. (English) Zbl 1129.68079

Seshia, Sanjit A.; Subramani, K.; Bryant, Randal E.

J. Satisf. Boolean Model. Comput. 3, No. 1-2, 67-90 (2007).

Summary: We consider the satisfiability problem for Boolean combinations of Unit two Variable Per Inequality (UTVPI) constraints. A UTVPI constraint is linear constraint containing at most two variables with non-zero coefficients, where furthermore those coefficients must be either \(-1\) or 1. We prove that if a satisfying solution exists, then there is a solution with each variable taking values in \([-n\cdot (b_{\max} + 1)\), \(n\cdot(b_{\max} + 1)]\) where \(n\) is the number of variables, and \(b_{\max}\) 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 can be used in a finite instantiation-based approach to deciding satisfiability of UTVPI formulas. An experimental evaluation demonstrates the efficiency of such an approach. One of our key results is to show that an integer point inside a UTVPI polyhedron, if one exists, can be obtained by rounding a vertex. As a corollary of this result, we also obtain a polynomial-time algorithm for approximating optima of UTVPI integer programs to within an additive factor.

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20	Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
90C05	Linear programming

Keywords:

unit two variable per inequality constraints; Boolean satisfiability; automated theorem proving; integer linear programming; decision procedures; constraint satisfaction; verification; optimization

Software:

BarcelogicTools; Octagon