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 variables of V′ are automatically generated. This is significant because these assignments can be applied, as though they were inferences, to simplify φ.

Second, some efficient operations based on these conditions are introduced and can be integrated into existing frameworks of both search-oriented and constraint-oriented methods of satisfiability. All of these operations are relaxations in the use of existential quantification and therefore may fail to find one or more existing safe assignments.

Finally, we compare and contrast the relationship of these operations to autarkies and present some preliminary results.