article · Journal on Satisfiability Boolean Modeling and Computation · 2006

Extending Existential Quantification in Conjunctions of BDDs

Sean Weaver, John Franco, John S. Schlipf

Cited by 15Open access

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.

Cite this paper

APA 7

Weaver, S., Franco, J., & Schlipf, J. S. (2006). Extending Existential Quantification in Conjunctions of BDDs. Journal on Satisfiability Boolean Modeling and Computation, 1(2), 89–110. https://doi.org/10.3233/sat190004

MLA 9

Weaver, Sean, et al. “Extending Existential Quantification in Conjunctions of BDDs.” Journal on Satisfiability Boolean Modeling and Computation, vol. 1, no. 2, 2006, pp. 89–110, https://doi.org/10.3233/sat190004.

Chicago

Weaver, Sean, John Franco, and John S. Schlipf. 2006. “Extending Existential Quantification in Conjunctions of BDDs.” Journal on Satisfiability Boolean Modeling and Computation 1 (2): 89–110. https://doi.org/10.3233/sat190004.

Harvard

Weaver, S., Franco, J. and Schlipf, J.S. (2006) ‘Extending Existential Quantification in Conjunctions of BDDs’, Journal on Satisfiability Boolean Modeling and Computation, 1(2), pp. 89–110. Available at: https://doi.org/10.3233/sat190004.

BibTeX

@article{weaver2006extending,
  title = {{Extending Existential Quantification in Conjunctions of BDDs}},
  author = {Weaver, Sean and Franco, John and Schlipf, John S.},
  journal = {Journal on Satisfiability Boolean Modeling and Computation},
  volume = {1},
  number = {2},
  pages = {89--110},
  year = {2006},
  doi = {10.3233/sat190004}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.