论文标题
通过证书条款消除部分量词
Partial Quantifier Elimination By Certificate Clauses
论文作者
论文摘要
在本报告中，我们研究了命题CNF公式的部分量化器消除（PQE）。 PQE是消除量词的概括，其中人们可以将量词范围限制为目标子句的一小部分。 PQE的吸引力是双重的。首先，PQE可以比全量化器消除更简单。其次，PQE提供了一种用于执行增量计算的语言。许多验证问题（例如等效检查和模型检查）本质上是增量的，因此可以通过PQE解决。我们的方法是基于仅取决于使目标子句$ \ mathit {冗余} $的未定量变量的定量变量的基础。证明目标条款的冗余是通过构建“证书”条款来完成的，这意味着前者。我们描述了一种称为$ \ mathit {start} $的PQE算法，该算法采用了上述方法。要评估$ \ Mathit {start} $，我们将其应用于连续电路$ n $的不变生成。不变生成的目的是找到$ n $的$ \ mathit {不需要的} $不变性，证明了本应达到的状态的不可行。如果$ n $有不想要的不变性，那就是越野车。我们使用FIFO缓冲区和HWMCC-13基准测试的实验表明，$ \ mathit {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.
