A decomposition method for CNF minimality proofs

•We describe a decomposition method for proving minimality of a CNF formula.•The method is general and can be used to any CNF formula.•The described method is demonstrated in proof of NP-hardness of minimizing a Horn CNF formula.•Then the described method is demonstrated in proof of NP-hardness of minimizing a Horn 3CNF formula.

A CNF is minimal if no shorter CNF representing the same function exists, where by CNF length we mean either the number of clauses or the total number of literals (sum of clause lengths). In this paper we develop a decomposition approach that can be in certain situations applied to a CNF formula when proving its minimality. We give two examples in which this decomposition approach is used. Both examples deal with pure Horn minimization, a problem defined as follows: given a pure Horn CNF, construct a logically equivalent pure Horn CNF which is the shortest possible (either w.r.t. the number of clauses or w.r.t. the total number of literals). Both presented examples give alternative proofs of known complexity results for pure Horn minimization.