Quantifier elimination by dependency sequents

摘要

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 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.