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.
(from crpit.com)
(local if available)