Optimisation Techniques for Combining Constraint Solvers

Stephan KepserStephan Kepser, Jörn RichtsJörn Richts

Datei:KepserRichts-Frocos-98.ps.gz

Download

Stephan Kepser, Jörn Richts
Optimisation Techniques for Combining Constraint Solvers
In Dov Gabbay and Maarten de Rijke, eds., Frontiers of Combining Systems 2, Papers presented at FroCoS'98, 193-210, 1999. Research Studies Press/Wiley

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 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.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ KepserRichts-Frocos-98,
  address = {Amsterdam},
  author = {Stephan {Kepser} and J{\"o}rn {Richts}},
  booktitle = {Frontiers of Combining Systems 2, Papers presented at FroCoS'98},
  editor = {Dov {Gabbay} and Maarten de {Rijke}},
  pages = {193--210},
  publisher = {Research Studies Press/Wiley},
  title = {Optimisation Techniques for Combining Constraint Solvers},
  year = {1999},
}