Local Computing By Partial Quantifier Elimination

Localization of computations plays a crucial role in solving hard problems efficiently. We will refer to the techniques implementing such localization as local computing. We relate local computing with partial quantifier elimination (PQE). The latter is a generalization of regular quantifier elimination where one can take a part of the formula out of the scope of quantifiers. The objective of this paper is to show that PQE can be viewed as a language of local computing and hence building efficient PQE solvers is of great importance. We describe application of local computing by PQE to three different problems of hardware verification: property generation, equivalence checking and model checking. Besides, we discuss using local computing by PQE for SAT solving. Finally, we relate PQE and interpolation, a form of local computing.