On Efficient Algorithms For Partial Quantifier Elimination
Eugene Goldberg
TL;DR
Partial Quantifier Elimination (PQE) generalizes QE by allowing a subset $G$ of clauses to be removed from the existential quantifier scope, solving $\exists{X}[F] \equiv H(Y) \wedge \exists{X}[F\\setminus G]$ with a quantifier-free $H(Y)$. The approach centers on redundancy-based reasoning with D-sequents; current solvers lack reuse of D-sequents, which the paper aims to remedy with two theoretical results enabling safe reuse of extended D-sequents and potential performance gains. The contributions align PQE with practical verification tasks such as model checking and property generation, promising significant speedups and scalability. The work also clarifies foundational definitions and outlines a path toward certificate clauses and extended D-sequents for robust reusability.
Abstract
Earlier, we introduced Partial Quantifier Elimination (PQE). It is a $\mathit{generalization}$ of regular quantifier elimination where one can take a $\mathit{part}$ of the formula out of the scope of quantifiers. We apply PQE to CNF formulas of propositional logic with existential quantifiers. The appeal of PQE is that many problems like equivalence checking and model checking can be solved in terms of PQE and the latter can be very efficient. The main flaw of current PQE solvers is that they do not $\mathit{reuse}$ learned information. The problem here is that these PQE solvers are based on the notion of clause redundancy and the latter is a $\mathit{structural}$ rather than $\mathit{semantic}$ property. In this paper, we provide two important theoretical results that enable reusing the information learned by a PQE solver. Such reusing can dramatically boost the efficiency of PQE like conflict clause learning boosts SAT solving.