Partial Quantifier Elimination By Certificate Clauses
Eugene Goldberg
TL;DR
The paper introduces Partial Quantifier Elimination (PQE) for propositional CNF and presents START, a redundancy-based PQE solver that uses certificate clauses to prove target clauses redundant. By extracting free, equisatisfiable certificates and employing blocked-clause theory, START enables incremental, subspace-based reasoning for PQE and QE generalization. The approach is demonstrated on invariant generation for sequential circuits, enabling automatic discovery of unwanted invariants and bug detection that are hard for existing methods; experiments with FIFO buffers and HWMCC-13 benchmarks show START solving a substantial portion of PQE tasks more effectively than prior DS-PQE and withstands QE-based comparisons where QE often fails within practical time limits. The work highlights PQE as a viable tool for incremental verification tasks and bug detection, offering a path toward scalable invariant generation and targeted QE in hardware verification contexts.
Abstract
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.