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

CC BY-SA 3.0
2015-02-25T19:02:09.593Z
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.
Martin Seymour
CC BY-SA 3.0
2015-02-25T21:35:15.543Z
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.
Yuval Filmus
CC BY-SA 3.0
2015-02-26T06:13:12.717Z
@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 [cs.se]. You can flag the question and ask mods to move it there.
Kaveh
CC BY-SA 3.0
2015-02-25T06:19:51.717Z
2015-02-25T06:19:51.717Z
Yuval Filmus
<p>A simple algorithm for Horn-SAT (in CNF) is the following:</p>

<p><em>Given</em>: A Horn formula $\phi$ in CNF.</p>

<p>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.</p>

<p>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).</p>

<p>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.</p>

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

<cc.complexity-theory><sat><logspace>
Why can't Horn-SAT be solved in Log-space?
Martin Seymour
# Why can't Horn-SAT be solved in Log-space?

(Asked by: username_0 on 2015-02-25)

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?

**Tags:** cc.complexity-theory, sat, logspace


---

## 1 answers

### Answer by username_1 on 2015-02-25. Score: 2

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

> **Comments:**
> **username_0**: I asked a question, username_1 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.  
> **username_1**: 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.  
> **username_2**: @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 [cs.se]. You can flag the question and ask mods to move it there.  

---

