Optimisation Techniques for Combining Constraint Solvers

S. KepserS. Kepser, J. RichtsJ. Richts

Datei:LTCS-Rep-96-04.ps.gz

Download

S. Kepser, J. Richts
Optimisation Techniques for Combining Constraint Solvers
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-96-04, 1996. LTCS-Report

Details
Bibtex

KurzfassungAbstract
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 two optimisation methods, called the iterative and the deductive method. The iterative method reorders and localises the non-deterministic decisions. The deductive method uses specific algorithms for the components to reach certain decisions deterministically. 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.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ KepserRichts-LTCS-96-04,
  address = {Germany},
  author = {S. {Kepser} and J. {Richts}},
  institution = {LuFG Theoretical Computer Science, RWTH Aachen},
  number = {LTCS-96-04},
  title = {Optimisation Techniques for Combining Constraint Solvers},
  type = {LTCS-Report},
  year = {1996},
}