Semantical and computational aspects of Horn approximations

Selman and Kautz proposed a method, called Horn approximation, for speeding up inference in propositional Knowledge Bases. Their technique is based on the compilation of a propositional formula into a pair of Horn formulae: a Horn Greatest Lower Bound (GLB) and a Horn Least Upper Bound (LUB). In thi s paper we focus on GLBs and address two questions that have been only marg inally addressed so far: (1) what is the semantics of the Horn GLBs? (2) what is the exact complexity of finding them? We obtain semantical as well as computational results. The major semantical result is: The set of minimal models of a propositional formula and the se t of minimum models of its Horn GLBs are the same. The major computational result is: Finding a Horn GLB of a propositional formula in CNF is NP-equiv alent, (C) 2000 Elsevier Science B.V. All rights reserved.