A decomposition method for CNF minimality proofs

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.

Authors

• Endre Boros
• Ondřej Čepek Charles University, Faculty of Mathematics and Physics, Department of Theoretical Computer Science and Mathematical Logic
• Petr Kučera Charles University

Keywords

• Boolean functions
• CNF
• Boolean minimization
• Horn minimization
• Decomposition method