Partial Quantifier Elimination By Certificate Clauses

We study partial quantifier elimination (PQE) for propositional CNF formulas. In contrast to full quantifier elimination, in PQE, 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 property generation of a sequential circuit $N$. The goal of property generation is to find a $\mathit{bad}$ property of $N$ proving unreachability of a state that is supposed to be reachable. If $N$ has a bad property, it is buggy. Our experiments with FIFO buffers and HWMCC-13 benchmarks suggest that $\mathit{START}$ can be used for detecting bugs in real-life designs.