Name
Abstract | ||
|---|---|---|
We consider the problem of elimination of existential quantifiers from a Boolean CNF formula. Our approach is based on the following observation. One can get rid of dependency on a set of variables of a quantified CNF formula F by adding resolvent clauses of F eliminating boundary points. This approach is similar to the method of quantifier elimination described in [9]. The difference of the method described in the present paper is twofold: {\bullet} branching is performed only on quantified variables, {\bullet} an explicit search for boundary points is performed by calls to a SAT-solver Although we published the paper [9] before this one, chrono- logically the method of the present report was developed first. Preliminary presentations of this method were made in [10], [11]. We postponed a publication of this method due to preparation of a patent application [8]. |
Year | Venue | Field |
|---|---|---|
2012 | CoRR | Quantifier elimination,Discrete mathematics,Resolvent,Algorithm,Mathematics,Branching (version control) |
DocType | Volume | Citations |
Journal | abs/1204.1746 | 2 |
PageRank | References | Authors |
0.39 | 8 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eugene Goldberg | 1 | 25 | 8.01 |
| Panagiotis Manolios | 2 | 634 | 53.62 |