1
$\begingroup$

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.
Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
1
$\begingroup$

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

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$
    – csTheoryBeginner
    May 7, 2018 at 15:45
  • $\begingroup$ @csTheoryBeginner, that's not a HornSAT formula. $\endgroup$
    – D.W. ♦
    May 7, 2018 at 15:54
  • $\begingroup$ 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. $\endgroup$
    – csTheoryBeginner
    May 7, 2018 at 16:28
  • $\begingroup$ @csTheoryBeginner, well, that's a different question. Sorry, but this site format doesn't work well for back-and-forth interaction. If you have a different question or a follow-up question, please use the 'Ask Question' button in the upper-right (and provide full context and make sure you've thought about it before asking and show us what you tried and your reasoning, as usual), rather than asking it in the comments. $\endgroup$
    – D.W. ♦
    May 7, 2018 at 17:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.