On computing minimal models

This paper addresses the problem of computing the minimal models of a given CNF propositional theory. We present two groups of algorithms. Algorithms in the first group are efficient when the theory is almost Horn, that is, when there are few non-Horn clauses and/or when the set of all literals that appear positive in any non-Horn clause is small. Algorithms in the other group are efficient when the theory can be represented as an acyclic network of low-arity relations. Our algorithms suggest several characterizations of tractable subsets for the problem of finding minimal models.