Boolean Affine Approximation with Binary Decision Diagrams

Henshall, K., Schachte, P., Sondergaard, H. and Whiting, L.

    Selman and Kautz's work on knowledge compilation has established how approximation (strengthening and/or weakening) of a propositional knowledgebase can be used to speed up query processing, at the expense of completeness. In the classical approach, the knowledge-base is assumed to be presented as a propositional formula in conjunctive normal form (CNF), and Horn functions are used to overand under-approximate it (in the hope that many queries can be answered efficiently using the approximations only). However, other representations are possible, and functions other than Horn can be used for approximations, as long as they have deduction-computational properties similar to those of the Horn functions. Zanuttini has suggested that the class of affine Boolean functions would be especially useful in knowledge compilation and has presented various affine approximation algorithms. Since CNF is awkward for presenting affine functions, Zanuttini considers both a sets-of-models representation and the use of modulo 2 congruence equations. Here we consider the use of reduced ordered binary decision diagrams (ROBDDs), a representation which is more compact than the sets of models and which (unlike modulo 2 congruences) can express any source knowledge-base. We present an ROBDD algorithm to find strongest affine upper-approximations of a Boolean function and we argue its correctness.
Cite as: Henshall, K., Schachte, P., Sondergaard, H. and Whiting, L. (2009). Boolean Affine Approximation with Binary Decision Diagrams. In Proc. Fifteenth Computing: The Australasian Theory Symposium (CATS 2009), Wellington, New Zealand. CRPIT, 94. Downey, R. and Manyem, P., Eds. ACS. 119-127.
pdf (from crpit.com) pdf (local if available) BibTeX EndNote GS