Counting solutions of a particular type in HORN SAT I am interested in counting the number of solutions of a particular type (say #) in HORN SAT. I have 2 questions concerning the same.


Suppose we have a HORN SAT -: $(x_1) \land (x_2 \implies x_1)$, then the solutions are $(1, 0)$ and $(1,1)$. For solutions of type #, I would like to eliminate $(1,1)$ as after negating $x_2$ we will still have a valid solution. In some sense $(1,1)$ is not a minimal solution. Do solutions of type # have a formal name? It seems natural that SAT solvers must strive to obtain solutions of type # and use those to generate other solutions.
Since the problem of HORN satisfiability is easy, are there efficient algorithms for counting HORN sat solutions? If so, could someone please point me to a good reference.
Finding the minimal solution can be done in polynomial time (in fact, linear time), using the standard algorithm.  There is always only a single minimal solution, and the standard algorithm for testing satisfiability of a HornSAT instance will also give you the minimal solution.

Counting the number of solutions is #P-complete and thus seems to be quite hard; see Is #HORNSAT polynomial?.