A solution domain is an algebraic structure which is used to interpret the constraint language. The solution domains we will be looking at are always infinite. This certainly constitutes a restriction, especially since there are many efficient constraint solving techniques for finite domains, but the infiniteness of the domain is required for our type of combination. Still, not every infinite domain will be right for our purposes. We are interested in symbolic, non-numerical solution domains of a fairly general character. Solution domains that fulfil these properties and are suitable for combination are called quasi-free structures. We will explain this notion, that was introduced by F. Baader and K. U. Schulz, later. Quasi-free structures generalise free structures and hence comprise solution domains such as term algebras and quotien term algebras. But also vector spaces, rational tree algebras, well-founded and non-wellfounded lists, sets and multi sets are quasi-free structures. This shows that many important non-numerical infinite solution domains are indeed covered.
A constraint solver is an algorithm that decides the constraint language or a fragment of it. In other words, given a formula, the constraint solver states whether the formula holds true in the solution domain. Very often, constraints are just conjunctions of atomic formulae, variables appearing in them are thought of as being implicitely existentially quantified. Other fragments we will consider are the existential fragment -- conjunctions and disjunctions of atoms and negated atoms -- and the positive theory, which permits arbitrary quantification of conjunctions and disjunctions of atoms.
Given these constraint systems, we are interested in systematic ways of combining them. A combination is systematic, if it provides the following. It gives an explicit construction mechanism to gain a combined solution domain given the solution domains of the components. The combined solution domain should again be a quasi-free structure, and it should share relevant structural properties with its components. Secondly, there must be an algorithm that solves ``mixed'' constraints in the combined solution domain by reducing them to pure constraints in the components in such a way that a mixed constraint is valid in the combined solution domains if and only if the corresponding pure constraints are valid in the component solution domains. We also demand conservativeness in the sense that a pure constraint over the language of just one component is true in the combined solution domain if and only if it is true in the component. Evaluation of pure constraints should not lead to new results.
An important restriction in combination concerns the signatures of the component systems. A signature comprises the sets of constants, function and predicate symbols that are used to construct the constraint language. In the combinations we will look at, we always assume the signatures to be disjoint, i.e., to share no constants, function or predicate symbols, even if we do not state so explicitely. This restriction may seem severe, but to date no-one has come up with decent results on combining constraint systems over non-disjoint signatures.
We start with the description of quasi-free structures and the free amalgamated product. We quote here work by F. Baader and K. U. Schulz to introduce concepts and notions fundamental to our work. Quasi-free structures are the solution domains we assume in our constraint systems. As generalisations of free structures, they comprise many important non-numerical infinite solution domains such as term algebras and quotient term algebra, rational tree algebras, hereditarily finite well-founded and non-wellfounded lists, sets and multi sets, vector spaces, and certain feature structures. Quasi-free structures have a simple, purely algebraic definition. While in a free structure, every element of the domain must be finitely generated, this is no longer required with quasi-free structures. It suffices that each element has a kind of a ``handle'' that can be used to determine the image of this element under an arbitrary homomorphism.
The free amalgamated product constitutes a first systematic way to combine constraint systems. It comes equipped with a general method that, given two arbitrary quasi-free structures, constructs a combined solution domain and a decomposition algorithm to solve ``mixed'' constraints, i.e., constraints built over the language of the joint signature, by reducing them to pure constraints in the components. The free amalgamated product as solution domain is characterised by the important property of being the most general combination of two quasi-free structures in the sense that every other combination contains a homomorphic image of it. To show the above demanded conservativeness, we present the theorem that the reduct of the free amalgamated product to one component signature is isomorphic to the component structure. The decomposition algorithm translates mixed constraints over the joint signature into pure constraints of the component signatures in such a way, that a solution for a mixed constraint exists in the free amalgamated product if and only if there are solutions of the translated pure constraints in the component domains. The core of the algorithm consists of three non-deterministic steps that guess an information exchange about variables occurring in both components' constraints after translation. On the base of this algorithm, Baader and Schulz show that the positive fragment of the constraint language of the joint signature is decidable in the free amalgamated product, provided the positive fragments of the component constraint languages over their signatures are both decidable.
Our first own contribution examines this decomposition algorithm and provides optimisation techniques therefor. The three non-deterministic steps mentioned above span a search space that huge that in a practical implementation, even small constraint problems are intractable. To overcome this problem, one has to find methods which drastically shrink the search space. Our interest was to find general methods that should be applicable to a wide range of quasi-free structures and their constraint solvers. Two such optimisation method are presented, called the iterative and the deductive method. The iterative method is designed for the combination of more than two constraint solvers; and the higher the number of solvers combined, the more important this method becomes. It is based on the observation, that the original decomposition algorithm largely expands the search space in such a case, because it makes all non-deterministic decisions for all components first, before testing the first component problem for solvability. The iterative method localises non-deterministic choices, it tries to solve a single component first by guessing those non-deterministic choices that are relevant for that component and proceeds to the next component only after it could solve the current one. The difficulty of this simple idea lies in proving that the thus amended decomposition algorithm is still correct and complete, i.e., that the mixed constraints have a solution if and only if the the iterative method finds one for each pure component problem.
The deductive method is based on the insight that not every decision has to be made non-deterministically. Indeed, one can find that in many cases the constraint problem at hand and the component solution domains and constraint solvers determine certain choices in the sense that only if they are made in one particular way, the problem is solvable. To use the deductive method, one needs new component constraint solvers, which have to do more than just decide whether a pure constraint problem is solvable. They must be capable of computing which choices have to be made deterministically in what way in order to keep their component problem solvable. The combination algorithm hence becomes kind of a moderator. It asks the component solvers, which decisions can be made deterministically and in what way, percolating these informations from component solver to component solver. Only after no new decisions can be made deterministically, it picks one non-deterministic choice. Thereafter it starts again consulting the component solvers, and so on, until all decisions are made. If then still all component solvers state their pure constraint problem is solvable, then the original mixed problem has a solution.
Since the two optimisation methods are totally independent of each other, one can easily integrate them into a common system. In order to test the efficiency of the optimisation, we implemented several versions of them. The test results provided show that many problems can be solved several orders of magnitude faster than with the original algorithm by Baader and Schulz. And there are some examples that cannot be solved in reasonable time without the optimisation methods.
The second contribution introduces the concept of rational amalgamation. It establishes a second systematic way of combining constraint systems. Although the free amalgamated product is the most general combination method, there are examples of combination that are not instances of the free amalgamated product. Work by A. Colmerauer on the combination of rational tree algebras and rational nested lists and work by W. Rounds and A. Moshier and C. Pollard on the combination of feature structures and non-wellfounded sets are such examples. In all of these cases, the component structures are ``rational'', they contain infinite (but periodic) elements. In such a situation, the free amalgamated product is not the combination of choice, because the elements in the combined solution domain are always finite. Mixed constraints that demand an infinite number of transitions from one component to the other are therefore unsolvable in the free amalgamated product.
This is where rational amalgamation steps in. It provides a combined solution domain that contains rational elements and hence allows to solve such mixed constraints. Therefore, rational amalgamation is the method of choice when combining constraint domains that are themselves rational. It comes equipped with a general construction method for a rational combined solution domain, given two arbitrary so-called non-collapsing quasi-free structures. For this combined solution domain, we show that the reduct to just one component signature is isomorphic to that component domain ensuring in this way the demanded conservativeness. We proof that the free amalgamated product is -- up to isomorphism -- a substructure of rational amalgamation. The following theorem shows the naturalness of the construction, too: the rational amalgamation of two rational tree algebras over disjoint signatures is isomorphic to the rational tree algebra of the joint signatures. The decomposition algorithm for rational amalgamation is a simplified variant of the one for the free amalgamated product; the final of the three non-deterministic steps is not required in rational amalgamation. Using this decomposition algorithm, we show that solvability of mixed constraints is decidable in the rational amalgamation, if solvability of pure constraints (with certain technical requirements) is decidable in both component domains. For the special class of rational non-collapsing structures, the positive existential theory of the rational amalgamation is decidable, if the positive universal-existential theory is decidable in both components.
Finally, we deal with negation in combining constraint systems. The constraints we mentioned so far were exclusively positive constraints, they contained neither negation nor implication. But clearly, implication is a desirable tool when formulating constraint problems. For example, constraint entailment cannot be expressed without it. And constraint entailment is used to decide whether one constraint subsumes or entails another when reducing constraints in a constraint solver (see, e.g., the constraint solver Oz). Negation is also an important part of the constraint language in Prolog II and III. Thus we investigate combinations of constraint systems that contain negation in their constraint languages in a first part of this chapter. The combined solution domain we use is again the free amalgamated product, and the algorithm is an extension of the decomposition algorithm to handle negative formulae, but one that does not introduce new non-deterministic steps. We show that the existential theory of the free amalgamated product over the joint signatures is decidable, if the existential theories of both components (with certain technical restrictions) are decidable. Furthermore we give conditions for the solutions in the components under which there exists a ground solution in the free amalgamated product, since there is a special interest in ground solutions, if the constraint problems contain negation. Work by R. Treinen lets us see that in general, it is not possible to solve a larger quantifier fragment in the free amalgamated product than just the existential one, even if one can solve a larger fragment in the components. We also show that Rational Amalgamation is in general a solution domain not suited for the combination of constraint systems with negation.
The second part of this chapter deals with the so-called independence property of negative constraints. A constraint system has the independence property, iff for every conjunction of positive constraints and every conjunction of negative constraints we have: The two conjunctions together are solvable if and only if for each negative constraint the conjunction of positive constraints plus that negative constraint is solvable. In this case, the negative constraints can be solved separately. This property is very important for real world constraint solvers. It enables the development of constraint solvers that solely solve positive constraints and can still handle negative ones by some means of translation. Firstly ignoring combination, we investigate which quasi-free structures own the independence property. Especially we consider equational theories, since they are an important subclass of quasi-free structures. For equational theories, we show that unitary theories have the independence property, while finitary do not. There theories of type 0 that own the independence property. For the combination of equational theories, one gains the following modularity result: The free amalgamated product of two unitary, regular and collapse-free equational theories is again unitary, and hence as the independence property. Generalising to quasi-free structures, we find that unitary structures have the independence property. And there are infinitary structures with the independence property. Finally, we lift the modularity result to the combination of quasi-free structures. The free amalgamated product of two unitary, regular and non-collapsing quasi-free structures is again unitary, and thus has the independence property.