Counting solutions of a particular type in HORN SAT

Question

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

1. 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.
2. 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.