Special-purpose quantifier 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.
Erika Cetindag, Martin Griebl