Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
An Efficient Decision Procedure for UTVPI Constraints
verfasst von : Shuvendu K. Lahiri, Madanlal Musuvathi
Erschienen in: Frontiers of Combining Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
A unit two variable per inequality (UTVPI) constraint is of the form
a
.
x
+
b
.
y
≤
d
where
x
and
y
are integer variables, the coefficients
a
,
b
∈ {–1,0,1} and the bound
d
is an integer constant. This paper presents an efficient decision procedure for UTVPI constraints. Given
m
such constraints over
n
variables, the procedure checks the satisfiability of the constraints in
O
(
n
.
m
) time and
O
(
n
+
m
) space. This improves upon the previously known
O
(
n
2
.
m
) time and
O
(
n
2
) space algorithm based on transitive closure. Our decision procedure is also equality generating, proof generating, and model generating.