Optimisation Techniques for Combining Constraint Solvers

Stephan Kepser and Jörn Richts

To appear in Frontiers of Combining Systems, Proceedings 98. Maarten de Rijke and Dov Gabbay (Eds.). Kluwer Academic Publishers, 1998.

In recent years, techniques that had been developed for the combination of unification algorithms for equational theories were extended to combining constraint solvers. These techniques inherited an old deficit that was already present in the combination of equational theories which makes them rather unsuitable for practical use: The underlying combination algorithms are highly non-deterministic. This paper is concerned with the practical problem of how to optimise the combination method of Baader and Schulz. We present an optimisation method, called the deductive method, which uses specific algorithms for the components to reach certain decisions deterministically. We also give a strategy how to select an order of non-deterministic decisions. Run time tests of our implementation indicate that the optimised combination method yields combined decision procedures that are efficient enough to be used in practice.