94-50 Restricted consensus method and quadratic implicates of pure Horn functions

DIMACS TR: 94-50

Restricted consensus method and quadratic implicates of pure Horn functions

Author: Ondrej Cepek

ABSTRACT
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: ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1994/94-50.ps

DIMACS Home Page