Earlier, we introduced Partial Quantifier Elimination (PQE). It is a $\mathit{generalization}$ of regular quantifier elimination where one can take a $\mathit{part}$ of the formula out of the scope of quantifiers. We apply PQE to CNF formulas of propositional logic with existential quantifiers. The appeal of PQE is that many problems like equivalence checking and model checking can be solved in terms of PQE and the latter can be very efficient. The main flaw of current PQE solvers is that they do not $\mathit{reuse}$ learned information. The problem here is that these PQE solvers are based on the notion of clause redundancy and the latter is a $\mathit{structural}$ rather than $\mathit{semantic}$ property. In this paper, we provide two important theoretical results that enable reusing the information learned by a PQE solver. Such reusing can dramatically boost the efficiency of PQE like conflict clause learning boosts SAT solving.

翻译：先前，我们引入了部分量词消去（PQE）方法。这是常规量词消去的一种$\mathit{泛化}$形式，允许将公式的$\mathit{部分}$内容移出量词的作用域。我们将PQE应用于带有存在量词的命题逻辑合取范式公式。PQE的吸引力在于，诸如等价性检验和模型检验等许多问题均可通过PQE求解，且后者可能具有极高效率。当前PQE求解器的主要缺陷在于无法$\mathit{重用}$已学习的信息。其根源在于这些求解器基于子句冗余性的概念，而冗余性属于$\mathit{结构}$性质而非$\mathit{语义}$性质。本文提出两项重要的理论结果，使得PQE求解器能够重用已学习的信息。这种重用机制可显著提升PQE的效率，其效果类似于冲突子句学习对SAT求解的加速作用。