DIMACS TR: 94-50
Restricted consensus method and quadratic implicates of pure
Author: Ondrej Cepek
In this paper we deal with a special subclass of Boolean functions -
the pure Horn functions. First we prove for this subclass a variant of
the well-known Quine theorem which has a certain ``non-expanding''
property (every clause resulting from a consensus has a degree bounded
by the maximum degree of a clause in the input CNF). Then we show how
to use this result for generating all quadratic implicates of a given
pure Horn function and we prove that the generating algorithm has the
best possible worst case complexity.
Paper available at:
DIMACS Home Page