Abstract
The problem of Horn Minimization (HM) can be stated as follows: given a Horn CNF representing a Boolean function f, find a shortest possible (optimally compressed) CNF representation of f, i.e., a CNF representation of f which consists of the minimum possible number of clauses. This problem is the formalization of the problem of knowledge compression for speeding up queries to propositional Horn expert systems, and it is known to be NP-hard. There are two subclasses of Horn functions for which HM is known to be solvable in polynomial time: acyclic and quasi-acyclic Horn functions. In this paper we define a new class of Horn functions properly containing both of the known classes and design a polynomial time HM algorithm for this new class.