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.
quantifier elimination dependency sequents resolution model checking sat