2012/04/08 by Eugene Goldberg, Goldberg, Eugene, Panagiotis Manolios +1
Computer Science · #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #cs.DM #cs.LO
paper · pdf · doi:10.48550/arxiv.1204.1746
The only change with respect to the previous version is a modification of the acknowledgement section
openalex publication_date 2012/04/08 · arxiv created 2012/06/05 · arxiv updated 2012/06/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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].