Quantifier Elimination via Clause Redundancy
Eugene Goldberg and Panagiotis Manolios.
We consider the problem of existential quantifier elimination for
Boolean CNF formulas. We present a new method for solving this problem
called Derivation of Dependency-Sequents (DDS). A Dependency-sequent
(D-sequent) is used to record that a set of quantified variables is
redundant under a partial assignment. We introduce the join operation
that produces new D-sequents from existing ones. We show that DDS is
compositional, i.e., if our input formula is a conjunction of
independent formulas, DDS automatically recognizes and exploits this
information. We introduce an algorithm based on DDS and present
experimental results demonstrating its potential.