  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].
