Sipser exercise : variant of CNF is NL-complete

Question

I'm stuck rather badly on a Sipser exercise, 8.21 in my edition:

8.21 Let $CNF_{H1}$ = {<$\phi$> | $\phi$ is a satisfiable cnf-formula where each clause contains any number of positive literals and at most one negated literal. Furthermore, each negated literal has at most one occurrence in $\phi$}. Show that $CNF_{H1}$ is $NL$-complete.

My problem is, if we remove the second condition (each negated literal occurs at most once), the language becomes $P$-complete, so we must use that second condition to get anywhere, but I have no idea whatsoever how to do that? I can't even prove that the language is in $NL$.

To deal with a clause $\lnot x_1 \lor x_2 \lor ... \lor x_n$, all of my efficient algorithms convert it to the equivalent $\lnot x_2 \land ... \lnot x_n \Rightarrow \lnot x_1$, and use that form to deduce in some cases that $x_1$ must be false. With such an approach, however, the second condition can't possibly help. If the negated $\lnot x_1$ appears twice, it simply means that we have more opportunities to deduce that $x_1$ is false, which can't hurt the algorithm?

Answer 1

Let's assume for simplicity that each negated literal appears exactly once. Let $C_i$ be the clause containing $\lnot x_i$. Consider the graph whose vertices are the variables, and $x_i$ is connected to $x_j$ if $x_j \in C_i$. This is a kind of implication graph: in order to deduce that $x_i$ is false from $C_i$, we must have first deduced that $x_j$ was false from $C_j$.

Show that $x_i$ is forced to be false (i.e., unit propagation shows that $x_i$ has to be false) iff the set of vertices reachable from $x_i$ contains no directed cycle, something which can be checked in NL (using coNL=NL). The formula is unsatisfiable iff there exists a positive clause in which all variables are forced to be false (and so unit propagation gets stuck at this clause).

This shows that your problem is in NL. To show that it is NL-complete, reduce from directed reachability. Encode all edges incoming to $x_i$ by a clause of the form $\lnot x_i \lor \cdots$.