Entailment of Atomic Set Constraints is PSPACE-Complete
Author: Joachim Niehren and Martin Müller and Jean-Marc Talbot
Editor:
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 t1 $\subseteq$ t2
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 thus 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.
|