Abstrakt
In this paper we study relationships between CNF representations of a given Boolean function f and essential sets of implicates off. It is known that every CNF representation and every essential set must intersect.
Therefore the maximum number of pairwise disjoint essential sets off provides a lower bound on the size of any CNF representation off. We are interested in functions, for which this lower bound is tight, and call such functions coverable.
We prove that for every covetable function there exists a polynomially verifiable certificate (witness) for its minimum CNF size. On the other hand, we show that not all functions are covetable, and construct examples of non-covetable 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.