A simple algorithm for Horn-SAT (in CNF) is the following:

Given: A Horn formula $\phi$ in CNF.

Find a unit clause (a clause with one literal) $C_i$. $~$Set the variable $x_j$ appearing in $C_i$ to TRUE (FALSE) if the literal in $C_i$ is $x_j$ ($\neg x_j$) respectively. $~$ Adjust all other clauses accordingly. $~$ That is, if variable $x_j$ appears in a clause $C_k$ with the same polarity as in $C_i$, then $C_k$ is satisfied, hence remove $C_k$ from $\phi$. $~$ On the other hand, if the polarity is the opposite and the literal $x_j$ ($\neg x_j$) appears in $C_k$, then remove $x_j$ ($\neg x_j$) from $C_k$, respectively.

Repeat the above procedure until there are no more unit clauses in $\phi$. $~$ At this point, every clause in $\phi$ has at least one negative literal. $~$ Now $\phi$ is trivially satisfiable (just set all remaining variables to FALSE).

Seems to me that this algorithm can be solved in log-space. $~$ Let the first tape be the input tape and let Tape 2 be the working tape. $~$ In Tape 1, the tape head will go back and forth to modify $\phi$ (and $\phi$ will keep shrinking as the algorithm proceeds). $~$ In Tape 2, we only need to store the index $j$ of the variable that we are currently working with, its polarity in the unit clause, and some other (constant amount of) information.

It looks like this algorithm only needs log-space. $~$ Your comments?


1 Answer 1


Log-space computations can't modify the input tape. Otherwise you just get linear space.

  • $\begingroup$ I asked a question, Yuval Filmus quickly answered, and I accepted the answer. All done. Case closed. If the topic adds no "research value" to cstheory-SE, then just close the discussion and be done with it. What seems to be the problem? Why put it on hold and place it in limbo? I don't understand the moderation policy. $\endgroup$ Feb 25, 2015 at 19:02
  • $\begingroup$ Nothing is wrong with your question, it's just not a good fit for this site. It would have been perfect for cs.se. Perhaps the moderators could migrate it there. $\endgroup$ Feb 25, 2015 at 21:35
  • $\begingroup$ @Martin, please refer to help center. There is no way to directly go to closed without going through on-hold. As Yuval said this would be more suitable for Computer Science. You can flag the question and ask mods to move it there. $\endgroup$
    – Kaveh
    Feb 26, 2015 at 6:13

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