Extending Existential Quantification in Conjunctions of BDDs

Abstract. We introduce new approaches intended to speed up determining the satisfiability of a given Boolean formula expressed as a conjunction of Boolean functions. A common practice in such cases, when using constraint-oriented methods, is to represent the functions as BDDs, then repeatedly cluster BDDs containing one or more variables, and finally existentially quantify those variables away from the cluster. Clustering is essential because, in general, existential quantification cannot be applied unless the variables occur in only a single BDD. But, clustering incurs significant overhead and may result in BDDs that are too big to allow the process to complete in a reasonable amount of time. There are two significant contributions in this paper. First, we identify elementary conditions under which the existential quantification of a subset of variables V may be distributed over all BDDs without clustering. We show that when these conditions are satisfied, safe assignments to the var...

• Type: Journal
• Year: 2006
• Where: JSAT
• Authors: Sean Weaver, John V. Franco, John S. Schlipf
• Keywords: Boolean Formula, Existential Quantification, Incurs Significant Overhead, JSAT 2006