A certifying algorithm for lattice point feasibility in a system of UTVPI constraints

K. Subramani () and Piotr Wojciechowski ()
Additional contact information
K. Subramani: West Virginia University
Piotr Wojciechowski: West Virginia University

Journal of Combinatorial Optimization, 2018, vol. 35, issue 2, No 6, 389-408

Abstract: Abstract This paper is concerned with the design and analysis of a certifying algorithm for checking the lattice point feasibility of a class of constraints called unit two variable per inequality (UTVPI) constraints. A UTVPI constraint has at most two non-zero variables and the coefficients of the non-zero variables belong to the set $$\{+\,1,\ -\,1\}$$ { + 1 , - 1 } . These constraints occur in a number of application domains, including but not limited to program verification, abstract interpretation, and operations research. As per the literature, the fastest known model generating algorithm for checking lattice point feasibility in UTVPI constraint systems runs in $$O(m \cdot n+n^{2} \cdot \log n)$$ O ( m · n + n 2 · log n ) time and $$O(n^{2})$$ O ( n 2 ) space, where m represents the number of constraints and n represents the number of variables in the constraint system (Lahiri and Musuvathi, in: Proceedings of the 5th international workshop on the frontiers of combining systems (FroCos), lecture notes in computer science, vol 3717, pp 168–183, 2005). In this paper, we design and analyze a new algorithm for checking the lattice point feasibility of UTVPI constraints. The presented algorithm runs in $$O(m \cdot n)$$ O ( m · n ) time and $$O(m+n)$$ O ( m + n ) space. Additionally it is certifying in that it produces a satisfying assignment in the event that it is presented with feasible instances and refutations in the event that it is presented with infeasible instances. The importance of providing certificates cannot be overemphasized, especially in mission-critical applications. Our approaches for the lattice point feasibility problem in UTVPI constraint systems is fundamentally different from existing approaches for this problem; indeed, it is based on new insights into combining well-known inference rules for these systems.

Keywords: UTVPI constraints; Certificates; Rounding scheme; Difference constraints (search for similar items in EconPapers)
Date: 2018
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
http://link.springer.com/10.1007/s10878-017-0176-3 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:jcomop:v:35:y:2018:i:2:d:10.1007_s10878-017-0176-3

Ordering information: This journal article can be ordered from
https://www.springer.com/journal/10878

DOI: 10.1007/s10878-017-0176-3

Access Statistics for this article

Journal of Combinatorial Optimization is currently edited by Thai, My T.

More articles in Journal of Combinatorial Optimization from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().