Boolean functions with a simple certificate for CNF complexity

In this paper we study relationships between CNF representations of a given Boolean function $f$ and essential sets of implicates of $f$. It is known that every CNF representation and every essential set must intersect. Therefore the maximum number of pairwise disjoint essential sets of $f$ provides a lower bound on the size of any CNF representation of $f$. We are interested in functions, for which this lower bound is tight, and call such functions coverable. We prove that for every coverable function there exists a polynomially verifiable certificate (witness) for its minimum CNF size. On the other hand, we show that not all functions are coverable, and construct examples of non-coverable functions. Moreover, we prove that computing the lower bound, i.e. the maximum number of pairwise disjoint essential sets, is $NP$-hard under various restrictions on the function and on its input representation.