Structure-Aware Computing, Partial Quantifier Elimination And SAT

Virtually all efficient algorithms of hardware verification are somewhat formula-specific i.e, try to take into account the structure of the formula at hand. So, those algorithms can be viewed as $\mathit{structure}$-$\mathit{aware}$ $\mathit{computing}$ (SAC). We relate SAC and $\mathit{partial}$ $\mathit{quantifier}$ $\mathit{elimination}$ (PQE), a generalization of regular quantifier elimination. In PQE, one can take a $\mathit{part}$ of the formula out of the scope of quantifiers. Interpolation can be viewed as a special case of PQE. The objective of this paper is twofold. First, we want to show that new powerful methods of SAC can be formulated in terms of PQE. We use three hardware verification problems (testing by property generation, equivalence checking and model checking) and SAT to explain how SAC is performed by PQE. Second, we want to demonstrate that PQE solving $\mathit{itself}$ can benefit from SAC. To this end, we describe a technique meant for building structure-aware SAT solvers that paves the way to structure-aware PQE solving.