# Why can't Horn-SAT be solved in Log-space? [closed]

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?