Partial Quantifier Elimination By Certificate Clauses

We study partial quantifier elimination (PQE) for propositional CNF formulas. In contrast to complete quantifier elimination, in PQE, only a small subset of target clauses is taken out of the scope of quantifiers. The appeal of PQE is twofold. First, it 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. Second, PQE can be dramatically simpler than complete quantifier elimination. 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. We apply $\mathit{START}$ to generating properties of a design implementation. A generated property not implied by a design specification proves the latter $\mathit{incomplete}$. An unwanted property of this implementation displays a $\mathit{bug}$. Our experiments with HWMCC-13 benchmarks suggest that $\mathit{START}$ can be used for generating properties of real-life designs.