We study partial quantifier elimination (PQE) for propositional CNF formulas with existential quantifiers. PQE is a generalization of quantifier elimination where one can limit the set of clauses taken out of the scope of quantifiers to a small subset of clauses. The appeal of PQE is that many verification problems (e.g. equivalence checking and model checking) can be solved in terms of PQE and the latter can be dramatically simpler than full quantifier elimination. We show that PQE can be used for property generation that can be viewed as a generalization of testing. The objective here is to produce an $\mathit{unwanted}$ property of a design implementation thus exposing a bug. We introduce two PQE solvers called $\mathit{EG}$-$\mathit{PQE}$ and $\mathit{EG}$-$\mathit{PQE}^+$. $\mathit{EG}$-$\mathit{PQE}$ is a very simple SAT-based algorithm. $\mathit{EG}$-$\mathit{PQE}^+$ is more sophisticated and robust than $\mathit{EG}$-$\mathit{PQE}$. We use these PQE solvers to find an unwanted property (namely, an unwanted invariant) of a buggy FIFO buffer. We also apply them to invariant generation for sequential circuits from a HWMCC benchmark set. Finally, we use these solvers to generate properties of a combinational circuit that mimic symbolic simulation.

翻译：我们研究命题CNF公式（带存在量词）的部分量词消去（PQE）。PQE是量词消去的一种推广，允许将量词作用域外的子句集限制为少量子句。PQE的吸引力在于，许多验证问题（如等价性检查和模型检验）可通过PQE求解，且后者可能比完全量词消去简单得多。我们证明PQE可用于性质生成，这可以视为测试的推广。其目标是为设计实现生成一个$\mathit{不期望}$的性质，从而暴露缺陷。我们引入两种PQE求解器：$\mathit{EG}$-$\mathit{PQE}$和$\mathit{EG}$-$\mathit{PQE}^+$。$\mathit{EG}$-$\mathit{PQE}$是一种非常简单的基于SAT的算法。$\mathit{EG}$-$\mathit{PQE}^+$比$\mathit{EG}$-$\mathit{PQE}$更复杂且更鲁棒。我们使用这些PQE求解器为有缺陷的FIFO缓冲器寻找一个不期望的性质（即不期望的不变量）。我们还将它们应用于HWMCC基准测试集时序电路的不变量生成。最后，我们使用这些求解器生成组合电路的属性，以模拟符号仿真过程。