Quantifier Elimination by Dependency Sequents

TL;DR

This paper introduces a novel method called Derivation of Dependency-Sequents (DDS) for existential quantifier elimination in Boolean CNF formulas, leveraging dependency sequents and a join operation to improve efficiency and exploit formula independence.

Contribution

The paper presents DDS, a new approach for quantifier elimination using dependency sequents, with a resolution-like join operation and proven compositionality for independent formulas.

Findings

DDS effectively records variable redundancy under partial assignments.

The join operation produces new dependency sequents from existing ones.

Experimental results show DDS's potential in quantifier elimination tasks.

Abstract

We consider the problem of existential quantifier elimination for Boolean formulas in Conjunctive Normal Form (CNF). 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 a resolution-like operation called join that produces a new D-sequent from two existing D-sequents. We also 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.