Quantifier Elimination via Clause Redundancy
Eugene Goldberg and Panagiotis Manolios.
We consider the problem of existential quantifier elimination for
Boolean formulas in conjunctive normal form. Recently we presented a
new method for solving this problem based on the machinery of
Dependency sequents (D-sequents). The essence of this method is to add
to the quantified formula implied clauses until all the clauses with
quantified variables become redundant. A D-sequent is a record of the
fact that a set of quantified variables is redundant in some
subspace. In this paper, we introduce a quantifier elimination
algorithm based on a new type of D-sequents called clause D-sequents
that express redundancy of clauses rather than variables. Clause
D-sequents significantly extend our ability to introduce and
algorithmically exploit redundancy, as our experimental results show.