Abstract
We address the problem of enumerating (producing) all models of a given theory. We show that the enumeration task can be performed in time proportional to the product of the number of models and the effort needed to generate each model in isolation. In other words, the requirement of generating a new solution in each iteration does not in itself introduce substantial complexity. Consequently, it is possible to decide whether any tractably satisfiable formula has more than K solutions in time polynomial in the size of the formula and in K. In the special cases of Horn formulas and 2-CNFs, although counting is #P-complete, to decide whether the count exceeds K, is polynomial in K.