Generating all maximal models of a Boolean expression

We examine the computational problem of generating all maximal models of a Boolean expression in CNF. We give a resolution-like method that reduces th e unnegated variables of an expression while preserving its set of maximal models. We present an output-polynomial algorithm for the 2CNF case and we show that the problem cannot be solved in output-polynomial time in the cas e of Horn expressions, unless P = NP, despite an affinity of this case to t he recently subexponentially solved transversal hypergraph problem. The pro blem is of course trivial for 1-valid and anti-Horn expressions, and open f or exclusive-ors; it is NP-hard in all other cases. (C) 2000 Elsevier Scien ce B.V. All rights reserved.