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.