Home |
Personal Info |
Papers |
Teaching |
Links |
An Improved Tight Closure Algorithm for Integer Octagonal Constraints (TR)
Roberto Bagnara
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Patricia M. Hill
School of Computing
University of Leeds
Leeds, LS2 9JT
United Kingdom
Enea Zaffanella
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Abstract
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(n3) algorithm to compute the tight c losure of a set of UTVPI integer constraints.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.
[Page last updated on June 04, 2007, 14:22:43.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links