Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/s10703-014-0214-z | Formal Methods in Computer-Aided Design |
Keywords | DocType | Volume |
Quantifier elimination,Resolution,Model checking,SAT,Dependency sequents | Journal | 45 |
Issue | ISSN | ISBN |
2 | 0925-9856 | 978-1-4673-4832-4 |
Citations | PageRank | References |
0 | 0.34 | 21 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eugene Goldberg | 1 | 25 | 8.01 |
| Panagiotis Manolios | 2 | 634 | 53.62 |