Entailment of atomic set constraints is PSPACE-complete

Author

Niehren, Joachim ; Müller, Martin ; Talbot, Jean-Marc

Author_Institution

Saarlandes Univ., Saarbrucken, Germany

fYear

1999

fDate

1999

Firstpage

285

Lastpage

294

Abstract

The complexity of set constraints has been extensively studied over the last years and was often found quite high. At the lower end of expressiveness, there are atomic set constraints which are conjunctions of inclusions t₁⊆t₂ between first-order terms without set operators. It is well-known that satisfiability of atomic set constraints can be tested in cubic time. Also, entailment of atomic set constraints has been claimed decidable in polynomial time. We refute this claim. We show that entailment between atomic set constraints can express validity of quantified boolean formulas and is this PSPACE hard. For infinite signatures, we also present a PSPACE-algorithm for solving atomic set constraints with negation. This proves that entailment of atomic set constraints is PSPACE-complete for infinite signatures. In case of finite signatures, this problem is even DEXPTIME-hard

Keywords

Boolean functions; computability; computational complexity; decidability; DEXPTIME-hard; PSPACE hard; PSPACE-algorithm; PSPACE-complete; atomic set constraints entailment; complexity; decidable; inclusions; polynomial time; quantified boolean formulas; satisfiability; Automata; Logic programming; Polynomials; Testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 1999. Proceedings. 14th Symposium on

Conference_Location

Trento

ISSN

1043-6871

Print_ISBN

0-7695-0158-3

Type

conf

DOI

10.1109/LICS.1999.782623

Filename

782623