Combination of Constraint Solvers II: Rational Amalgamation

Stephan Kepser and Klaus U. Schulz

The paper appeared in: Proceedings CP'96, Springer LNCS 1118.

In a recent paper (Baader & Schulz: CP95), the concept of ``free amalgamation'' has been introduced as a general methodology for interweaving solution structures for symbolic constraints, and it was shown how constraint solvers for two components can be lifted to a constraint solver for the free amalgam. Here we discuss a second general way for combining solution domains, called rational amalgamation. In praxis, rational amalgamation seems to be the preferred combination principle if the two solution structures to be combined are ``rational'' or ``non-wellfounded'' domains. It represents, e.g., the way how rational trees and rational lists are interwoven in the solution domain of Prolog III, and a variant has been used by W. Rounds for combining feature structures and hereditarily finite non-wellfounded sets. We show that rational amalgamation is a general combination principle, applicable to a large class of structures. As in the case of free amalgamation, constraint solvers for two component structures can be combined to a constraint solver for their rational amalgam. From this algorithmic point of view, rational amalgamation seems to be interesting since the combination technique for rational amalgamation avoids one source of non-determinism that is needed in the corresponding scheme for free amalgamation.