On Solving Boolean Combinations of UTVPI Constraints
Sanjit A. Seshia
K. Subramani
Randal E. Bryant
10.1184/R1/6607898.v1
https://kilthub.cmu.edu/articles/journal_contribution/On_Solving_Boolean_Combinations_of_UTVPI_Constraints/6607898
We consider the satisfiability problem for Boolean combinations of unit two variable
per inequality (UTVPI) constraints.
Our result can be used in a nite instantiation-based approach to
deciding satisability of UTVPI formulas. An experimental evaluation demonstrates the
eciency 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.
2006-06-01 00:00:00
Unit two variable per inequality constraints
Boolean satisfiability
automated theorem proving
integer linear programming
decision procedures
constraint satisfaction
verification
optimization.