Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

Quantifier Elimination via Clause Redundancy

Eugene Goldberg and Panagiotis Manolios.
FMCAD, 2013


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.

PDF (517K)