# 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.

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.

• Thank you for the answer. I just wanted clarification on the minimal solution. Consider the following dual HORN formula-: $(x_1 \implies T) \land (x_2 \implies T) \land (T \implies (x_1 \lor x_2))$. Then the solutions to formula are $(1, 0), (0,1), (1,1)$. However there are 2 minimal solutions here, namely $(1,0), (0,1)$. What am I missing in understanding? – csTheoryBeginner May 7 '18 at 15:45
• How about the DUAL HORN formula-: $x_1 \lor x_2$. This has 2 minimal solutions $(0,1), (1,0)$. I am using Dual Horn instead of Horn, but as I understand, things are symmetric between the two. – csTheoryBeginner May 7 '18 at 16:28