Partial Quantifier Elimination By Certificate Clauses

We study a modification of the Quantifier Elimination (QE) problem called Partial QE (PQE) for propositional CNF formulas. 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 $\mathit{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 QE. We perform PQE by adding a set of clauses depending only on unquantified variables that make the target clauses redundant. Proving redundancy of a target clause is done by derivation of a "certificate" clause $\mathit{implying}$ the former. We implemented this idea in a PQE algorithm called $\mathit{START}$. It bears some similarity to a SAT-solver with conflict driven learning. A major difference here is that $\mathit{START}$ backtracks as soon as a target clause is proved redundant (even if no conflict occurred). We experimentally evaluate $\mathit{START}$ on a practical problem. We use this problem to compare PQE with QE and QBF solving.