基于证书子句的部分量词消去
Partial Quantifier Elimination By Certificate Clauses
AI总结：
本研究提出基于证书子句的命题CNF公式部分量词消去算法START，可用于时序电路不变式生成与缺陷检测，在FIFO缓冲器和HWMCC-13基准上表现出优于现有方法的缺陷发现能力。
摘要：
本报告研究命题CNF公式的部分量词消去（Partial Quantifier Elimination，简称PQE）。PQE是量词消去的一种推广，研究者可将从量词辖域中取出的子句集合限定为目标子句的一个小子集。PQE的吸引力体现在两方面：首先，PQE的实现难度可能远低于完全量词消去；其次，PQE为执行增量计算提供了一种语言。许多验证问题（例如等价性检查和模型检查）本质上是增量式的，因此可以通过PQE来求解。我们的方法基于推导仅依赖未量化变量的子句，这类子句可使目标子句变得冗余。目标子句的冗余性证明通过构造一个蕴含该目标子句的“证书”子句来完成。我们描述了一种名为START的PQE算法，该算法采用了上述方法。为了评估START，我们将其应用于时序电路N的不变式生成任务。不变式生成的目标是找到N的一个“非期望”不变式，用于证明一个本应可达的状态实际上不可达。如果N存在非期望不变式，则说明该电路存在缺陷。我们针对FIFO缓冲器和HWMCC-13基准测试集开展的实验表明，START可用于检测现有方法难以发现的缺陷。
英文摘要：
In this report, we study partial quantifier elimination (PQE) for propositional CNF formulas. 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 target clauses. The appeal of PQE is twofold. First, PQE can be dramatically simpler than full quantifier elimination. Second, PQE provides a language for performing incremental computations. Many verification problems (e.g. equivalence checking and model checking) are inherently incremental and so can be solved in terms of PQE. Our approach is based on deriving clauses depending only on unquantified variables that make the target clauses $\mathit{redundant}$. Proving redundancy of a target clause is done by construction of a "certificate" clause implying the former. We describe a PQE algorithm called $\mathit{START}$ that employs the approach above. To evaluate $\mathit{START}$, we apply it to invariant generation for a sequential circuit $N$. The goal of invariant generation is to find an $\mathit{unwanted}$ invariant of $N$ proving unreachability of a state that is supposed to be reachable. If $N$ has an unwanted invariant, it is buggy. Our experiments with FIFO buffers and HWMCC-13 benchmarks suggest that $\mathit{START}$ can be used for detecting bugs that are hard to find by existing methods.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
