Problem #43
Originator: Jean-Pierre Jouannaud
Date: April 1991
Summary:
Design a framework for combining constraint solving algorithms.
Design a framework for combining constraint solving algorithms.
Remark
Some particular cases have been attacked: In [BS92] it was shown how
decision procedures for solvability of unification problems can be combined.
In [BS93] a similar technique is applied to (unquantified) systems of
equations and disequations. In [Rin92] the combination of unification
algorithms is extended to the case where alphabets share constants. In related
work [Bou92], unification is performed in the combination of an
equational theory and membership constraints.
Some further progress is in [Rin92].
The combination approach of [BS92] has been extended in
[BS95a] to constraints involving predicate symbols other
that equality, and [BS95b] in turn extends this approach to
constraint-solving over solution domains that are not free structures. These
results are presented in a uniform framework by [BS98].
The work of [Rin92] has been extended
to the case of “shared constructors” by [DKR94].
Date: Mon Apr 27 12:05:20 MET DST 1998
Unification algorithms (and therefore also constraint solvers) cannot be
combined in polynomial time, as proved by Hermann and Kolaitis
in [HK96].
References
-
[Bou92]
-
Alexandre Boudet.
Unification in order-sorted algebras with overloading.
In Kapur [Kap92].
- [BS92]
-
Franz Baader and Klaus Schulz.
Unification in the union of disjoint equational theories: Combining
decision procedures.
In Kapur [Kap92].
- [BS93]
-
Franz Baader and Klaus Schulz.
Combination techniques and decision problems for disunification.
In Claude Kirchner, editor, 5th International Conference on
Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer
Science, pages 301–315, Montreal, Canada, June 1993.
Springer-Verlag.
- [BS95a]
-
Franz Baader and Klaus Schulz.
Combination of constraint solving techniques: An algebraic point of
view.
In Jieh Hsiang, editor, 6th International Conference on Rewriting Techniques and
Applications, volume 914 of Lecture Notes in Computer
Science, pages 352–366, Kaiserslautern, Germany, April 1995.
Springer-Verlag.
- [BS95b]
-
Franz Baader and Klaus Schulz.
On the combination of symbolic constraints, solution domains, and
constraint solvers.
In Ugo Montanari and Francesca Rossi, editors, Principles and
Practice of Constraint Programming, volume 976 of Lecture Notes in Computer
Science, Cassis, France, September 1995.
Springer-Verlag.
- [BS98]
-
Franz Baader and Klaus Schulz.
Combination of constraint solvers for free and quasi-free structures.
Theoretical Computer Science, 1998.
To appear.
- [DKR94]
-
E. Domenjoud, F. Klay, and C. Ringeissen.
Combination techniques for non-disjoint equational theories.
In A. Bundy, editor, 12th International Conference on Automated
Deduction, volume 814 of Lecture Notes in Computer
Science, pages 267–281, Nancy, France, 1994.
Springer-Verlag.
- [HK96]
-
Miki Hermann and P. G. Kolaitis.
Unification algorithms cannot be combined in polynomial time.
In M. A. McRobbie and J. K. Slaney, editors, 13th International
Conference on Automated Deduction,
Lecture Notes in Computer
Science, pages 246–260, New Brunswick, NJ, July/August 1996.
Springer-Verlag.
To appear in a special issue of
Information and
Computation.
- [Kap92]
-
Deepak Kapur, editor.
11th International Conference on Automated Deduction, volume
607 of Lecture Notes
in Computer Science, Saratoga Springs, NY, June 1992.
Springer-Verlag.
- [Rin92]
-
Christophe Ringeissen.
Unification in a combination of equational theories with shared
constants and its application to primal algebras.
In A. Voronkov, editor, International Conference on Logic
Programming and Automated Reasoning, volume 624 of Lecture Notes in
Artificial Intelligence, St. Petersburg, Russia, July 1992.
Springer-Verlag.