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在计算上非常困难。我们早期介绍了一种称为$\mathit{部分}$QE(或简称PQE)的QE泛化。PQE允许解除公式的$\mathit{部分}$量词。PQE的吸引力有两点。首先,许多重要问题可以通过PQE来解决。其次,如果只解除公式的一小部分,则PQE比QE要快得多。为了使PQE实用,需要一种验证由PQE求解器产生的解的算法。在本文中,我们描述了一种非常简单的基于SAT的验证器$\mathit{VerPQE}$并提供了一些实验结果。