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 ombination of equational theories which makes them rather unsuitable for pratical use: The underlying combination algorithms are highly non-deterministic. This paper is concerned with the pratical 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.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:78809 |
| Date | 18 May 2022 |
| Creators | Kepser, Stephan, Richts, Jörn |
| Publisher | RWTH Aachen |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:report, info:eu-repo/semantics/report, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | urn:nbn:de:bsz:14-qucosa2-785040, qucosa:78504 |
Page generated in 0.0024 seconds