Publication at Faculty of Mathematics and Physics |
2011
Abstract
In this paper we study a class of CQ Horn functions introduced in Boros et al. (2010). We prove that given a CQ Horn function f, the maximal number of pairwise disjoint essential sets of implicates of f equals the minimum number of clauses in a CNF representing f.
In other words, we prove that the maximum number of pairwise disjoint essential sets of implicates of f constitutes a tight lower bound on the size (the number of clauses) of any CNF representation of f.