An n3u Upper Bound on the Complexity for Deciding the Truth of a Presburger Sentence Involving Two Variables Bounded Only by Existential Quantifiers
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E80-D No.2 pp.223-231
- Publication Date
- 1997/02/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Category
- Algorithm and Computational Complexity
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Kuniaki NAOI, Naohisa TAKAHASHI, "An n3u Upper Bound on the Complexity for Deciding the Truth of a Presburger Sentence Involving Two Variables Bounded Only by Existential Quantifiers" in IEICE TRANSACTIONS on Information,
vol. E80-D, no. 2, pp. 223-231, February 1997, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e80-d_2_223/_p
Copy
@ARTICLE{e80-d_2_223,
author={Kuniaki NAOI, Naohisa TAKAHASHI, },
journal={IEICE TRANSACTIONS on Information},
title={An n3u Upper Bound on the Complexity for Deciding the Truth of a Presburger Sentence Involving Two Variables Bounded Only by Existential Quantifiers},
year={1997},
volume={E80-D},
number={2},
pages={223-231},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={February},}
Copy
TY - JOUR
TI - An n3u Upper Bound on the Complexity for Deciding the Truth of a Presburger Sentence Involving Two Variables Bounded Only by Existential Quantifiers
T2 - IEICE TRANSACTIONS on Information
SP - 223
EP - 231
AU - Kuniaki NAOI
AU - Naohisa TAKAHASHI
PY - 1997
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E80-D
IS - 2
JA - IEICE TRANSACTIONS on Information
Y1 - February 1997
AB - 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.
ER -
English
