On Efficient Algorithms For Partial Quantifier Elimination

TL;DR

This paper introduces theoretical advancements that enable reusing learned information in Partial Quantifier Elimination (PQE), significantly improving its efficiency for applications like model checking.

Contribution

It provides two key theoretical results that allow reusing learned information in PQE, addressing a major flaw in existing solvers.

Findings

Reusing learned information can dramatically boost PQE efficiency.

Theoretical results enable semantic reuse of clause redundancy information.

Enhanced PQE algorithms can improve model checking and equivalence checking.

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.