Counting solutions of a particular type in HORN SAT
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?.