×

zbMATH — the first resource for mathematics

An improved tight closure algorithm for integer octagonal constraints. (English) Zbl 1138.68474
Logozzo, Francesco (ed.) et al., Verification, model checking, and abstract interpretation. 9th international conference, VMCAI 2008, San Francisco, USA, January 7–9, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-78162-2/pbk). Lecture Notes in Computer Science 4905, 8-21 (2008).
Summary: Integer octagonal constraints (a.k.a. Unit Two Variables Per Inequality or UTVPI integer constraints) constitute an interesting class of constraints for the representation and solution of integer problems in the fields of constraint programming and formal analysis and verification of software and hardware systems, since they couple algorithms having polynomial complexity with a relatively good expressive power. The main algorithms required for the manipulation of such constraints are the satisfiability check and the computation of the inferential closure of a set of constraints. The latter is called tight closure to mark the difference with the (incomplete) closure algorithm that does not exploit the integrality of the variables. In this paper we present and fully justify an \(O(n ^{3})\) algorithm to compute the tight closure of a set of UTVPI integer constraints.
For the entire collection see [Zbl 1134.68006].

MSC:
68R10 Graph theory (including graph drawing) in computer science
68W05 Nonnumerical algorithms
90C35 Programming involving graphs or networks
Software:
PPL
PDF BibTeX XML Cite
Full Text: DOI