Approaches to parallel quantifier elimination
Andreas Dolzmann, Oliver Gloor, Thomas Sturm · 1998
Special-purpose quanti er elimination procedures for problems of low degree using virtual substitution of test terms have recently turned out to be applicable to a variety of non-trivial non-academic problems.We study parallel algorithms based on these methods for several parallelization environments: a Cray YMP4/T3D, a workstation cluster, and a multi-processor Sparc.Our implementations show remarkable though sublinear speed-ups in all these environments.