
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

An n^{3}u 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.E80D
No.2
pp.223231 Publication Date: 1997/02/25 Online ISSN:
DOI: Print ISSN: 09168532 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)>>
Summary:
We show that the truth of a prenex normal form Presburger sentence bounded only by existential quantifiers (or an EPPsentence) involving two variables can be decided in deterministic polynomial time. Specifically, an upper bound of the computation for the decision is O(n^{3}u), where n is the number of atoms of the EPPsentence, and u is the largest absolute value of all coefficients in the EPPsentence. 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 EPPsentence is an NPcomplete problem, when the number of variables is not fixed. Furthermore, whether the truth of an EPPsentence 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 EPPsentence 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 EPPsentence is triangulated.

