-3
$\begingroup$

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?

$\endgroup$

closed as off-topic by Yuval Filmus, R B, Kaveh, Marzio De Biasi, Emil Jeřábek supports Monica Feb 25 '15 at 10:00

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Yuval Filmus, R B, Kaveh, Marzio De Biasi, Emil Jeřábek supports Monica
If this question can be reworded to fit the rules in the help center, please edit the question.

2
$\begingroup$

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

$\endgroup$
  • $\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$ – Martin Seymour Feb 25 '15 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$ – Yuval Filmus Feb 25 '15 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 '15 at 6:13

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