Problem #68 (Solved !)
Originator: Hubert Comon
Date: June 1993
Summary:
Is satisfiability of set constraints with projection and boolean
operators decidable?
Consider the existential fragment of the theory
defined by a binary predicate symbol ⊆, a finite
set of function symbols f1,…, fn, the function
symbols ∩, ∪, ¬, and the projection symbols
fi,j−1 for j ≤ arity(fi).
Variables are interpreted as subsets of the Herbrand Universe.
With the obvious interpretation of these symbols, is satisfiability
of such formulas decidable?
Special cases have been solved in
[HJ90, AW92, BGW93, GTT93a].
Remark
This has been solved positively by
[CP94b].
Partial solutions have been given by
[GTT93b][CP94a][AKW93].
References
-
[AKW93]
-
A. Aiken, D. Kozen, and E. Wimmers.
Decidability of systems of set constraints with negative constraints.
Technical Report 93-1362, Computer Science Department, Cornell
University, 1993.
- [AW92]
-
A. Aiken and E. Wimmers.
Solving systems of set constraints.
In Andre Scedrov, editor, Seventh
Symposium on Logic in
Computer Science, pages 329–340, Santa Cruz, CA, June 1992.
IEEE.
- [BGW93]
-
Leo Bachmair, Harald Ganzinger, and Uwe Waldmann.
Set constraints are the monadic class.
In Moshe Y. Vardi, editor, Eigth
Symposium on Logic in
Computer Science, pages 75–83, Montreal, Canada, June 1993.
IEEE.
- [CP94a]
-
W. Charatonik and L. Pacholski.
Negative set constraints with equality.
In Samson Abramsky, editor, Ninth
Symposium on Logic in
Computer Science, pages 128–136, Paris, France, July 1994.
IEEE.
- [CP94b]
-
W. Charatonik and L. Pacholski.
Set constraints with projections are in NEXPTIME.
In Proceedings of the 35th Symposium on Foundations of
Computer Science, pages 642–653, 1994.
- [GTT93a]
-
Rémy Gilleron, Sophie Tison, and Marc Tommasi.
Solving systems of set constraints using tree automata.
In Patrice Enjalbert, Alain Finkel, and Klaus W. Wagner, editors,
Symposium on Theoretical Aspects of Computer Science, volume 665 of
Lecture Notes in
Computer Science, Würzburg, Germany, February 1993.
Springer-Verlag.
- [GTT93b]
-
Rémy Gilleron, Sophie Tison, and Marc Tommasi.
Solving systems of set constraints with negated subset relationships.
In Proc. 34th Symposium on Foundations of Computer Science,
pages 372–380, Palo Alto, CA, November 1993.
IEEE.
- [HJ90]
-
Nevin Heintze and Joxan Jaffar.
A decision procedure for a class of set constraints.
In John C. Mitchell, editor, Fifth
Symposium on Logic in
Computer Science, pages 42–51, Philadelphia, PA, June 1990.
IEEE.