Disjoint essential sets of implicates of a CQ Horn function.

Abstract

In this paper we study a class of CQ Horn functions introduced in [5]. We prove that given a CQ Horn function f, the maximal number of pair-wise 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 impliates of f constitutes a tight lower bound on the size (the number of clauses) of any CNF representation of f.

Keywords

• Disjoint
• essential
• implicates
• function