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 C1 in I(f) and C2 in I(f) at least one of C1 and C2 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 quasi-acyclic 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).