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},
}