On Efficient Algorithms For Partial Quantifier Elimination

Earlier, we introduced Partial Quantifier Elimination (PQE). It is a generalization of regular quantifier elimination where one can take a 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 reuse learned information. The problem here is that these PQE solvers are based on the notion of clause redundancy and the latter is a structural rather than 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.