Removal of Quantifiers by Elimination of Boundary Points
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].
Cite
@article{arxiv.1204.1746,
title = {Removal of Quantifiers by Elimination of Boundary Points},
author = {Eugene Goldberg and Panagiotis Manolios},
journal= {arXiv preprint arXiv:1204.1746},
year = {2012}
}
Comments
The only change with respect to the previous version is a modification of the acknowledgement section