
Coverable functions: definitions and
properties
 Ondrej Cepek
abstract

Let f be a Boolean function and I(f) a resolution closure
of the set of prime implicates of f. We say that subset E of
I(f) is an essential set of f if for every resolvent
C in E genereted by resolution from C_{1} in
I(f) and C_{2} in I(f) at least
one of C_{1} and C_{2} also belongs to
E. Let ess(f) denote the maximum number of pairwise
disjoint essential sets of implicates of f and cnf(f)
the minimum number of clauses needed to represent f by a CNF. It is
known that ess(f) constitutes a lower bound for
cnf(f). A function f is called coverable if
ess(f) =cnf(f). In this talk we shall show that
ess(f) can be equivalently defined using special type of
essential sets which are defined by the falsepoints of f. Moreover,
we shall show, that this reformulation provides a polynomial size
certificate for the value of ess(f) thus providing polynomially
verifiable lower bound for cnf(f) which is tight if f
is coverable. Finally, we shall concentrate on the class of Horn CNFs,
recall that certain subclasses of Horn CNFs (e.g. quadratic, acyclic, and
quasiacyclic CNFs) represent coverable functions, and exhibit an example
which shows that there exist a Horn function which is not coverable,
i.e. such that ess(f) < cnf(f).

