An n3u Upper Bound on the Complexity for Deciding the Truth of a Presburger Sentence Involving Two Variables Bounded Only by Existential Quantifiers

Kuniaki NAOI  Naohisa TAKAHASHI  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E80-D   No.2   pp.223-231
Publication Date: 1997/02/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Algorithm and Computational Complexity
Keyword: 
Presburger arithmetic,  automatic theorem prover,  computation complexity,  integer programming,  algorithm,  

Full Text: PDF(743.7KB)>>
Buy this Article



Summary: 
We show that the truth of a prenex normal form Presburger sentence bounded only by existential quantifiers (or an EPP-sentence) involving two variables can be decided in deterministic polynomial time. Specifically, an upper bound of the computation for the decision is O(n3u), where n is the number of atoms of the EPP-sentence, and u is the largest absolute value of all coefficients in the EPP-sentence. In the analysis for the upper bound, the random access machine is assumed for the machine model. Additionally, a uniform cost criterion is assumed. Deciding the truth of an EPP-sentence is an NP-complete problem, when the number of variables is not fixed. Furthermore, whether the truth of an EPP-sentence involving two or more variables can be decided in deterministic polynomial time, when the number of variables is fixed, or not has remained an open problem. We previously proposed a procedure for quickly deciding the truth of an EPP-sentence on the basis of a suggestion by D.C.Cooper. We found the upper bound by analyzing the decision procedure. The procedure can be applied to both automated correctness proof of specification in various design fields and detection of infeasible paths in a program. In the procedure, a matrix denoting coefficients of the variables in the EPP-sentence is triangulated.