Quantifier elimination (QE) is an important problem that has numerous applications. Unfortunately, QE is computationally very hard. Earlier we introduced a generalization of QE called $\mathit{partial}$ QE (or PQE for short). PQE allows to unquantify a $\mathit{part}$ of the formula. The appeal of PQE is twofold. First, many important problems can be solved in terms of PQE. Second, PQE can be drastically faster than QE if only a small part of the formula gets unquantified. To make PQE practical, one needs an algorithm for verifying the solution produced by a PQE solver. In this paper, we describe a very simple SAT-based verifier called $\mathit{VerPQE}$ and provide some experimental results.

翻译：量词消除（QE）是一个具有广泛应用的重要问题。然而，QE在计算上非常困难。此前，我们提出了一种称为部分QE（简称PQE）的QE泛化方法。PQE允许对公式的"部分"进行非量词化处理。PQE的吸引力体现在两个方面：其一，许多重要问题可以通过PQE求解；其二，若仅需对公式的一小部分进行非量词化处理，PQE的速度可能远超QE。为使PQE具备实用性，需要一种可验证PQE求解器所产生解的正确性算法。本文描述了一种基于SAT的极为简化的验证器——VerPQE，并给出了相关实验结果。