  |
Entailment of Atomic Set Constraints is PSPACE-Complete
Author: Joachim Niehren and Martin Müller and Jean-Marc TalbotEditor:
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_1\subseteq t_2$ 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 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, the problem is even DEXPTIME-hard.
|