If $\mathsf{L = NL}$, then there is a logspace algorithm that solves the decision version of 2-SAT.

  • Is $\mathsf{L = NL}$ known to imply that there is a logspace algorithm to obtain a satisfying assignment, when given a satisfiable 2-SAT instance as input?

  • If not, what about algorithms which use sub-linear space (in the number of clauses)?


1 Answer 1


Given a satisfiable 2-CNF $\phi$, you can compute a particular satisfying assignment $e$ by an NL-function (that is, there is an NL-predicate $P(\phi,i)$ that tells you whether $e(x_i)$ is true). One way to do that is described below. I will freely use the fact that NL is closed under $\mathrm{AC}^0$-reductions, hence NL-functions are closed under composition; this is a consequence of NL = coNL.

Let $\phi(x_1,\dots,x_n)$ be a satisfiable 2-CNF. For any literal $a$, let $a^\to$ be the number of literals reachable from $a$ by a directed path in the implication graph of $\phi$, and $\let\ot\leftarrow a^\ot$ the number of literals from which $a$ is reachable. Both are computable in NL.

Observe that $\let\ob\overline \ob a^\to=a^\ot$, and $\ob a^\ot=a^\to$, due to skew-symmetry of the implication graph. Define an assignment $e$ so that

  • if $a^\ot>a^\to$, then $e(a)=1$;

  • if $a^\ot<a^\to$, then $e(a)=0$;

  • if $a^\ot=a^\to$, let $i$ be minimal such that $x_i$ or $\ob x_i$ appears in the strongly connected component of $a$ (it cannot be both, as $\phi$ is satisfiable). Put $e(a)=1$ if $x_i$ appears, and $e(a)=0$ otherwise.

The skew-symmetry of the graph implies that $e(\ob a)=\ob{e(a)}$, hence this is a well-defined assignment. Moreover, for any edge $a\to b$ in the implication graph:

  • If $a$ is not reachable from $b$, then $a^\ot<b^\ot$, and $a^\to>b^\to$. Thus, $e(a)=1$ implies $e(b)=1$.

  • Otherwise, $a$ and $b$ are in the same strongly connected component, and $a^\ot=b^\ot$, $a^\to=b^\to$. Thus, $e(a)=e(b)$.

It follows that $e(\phi)=1$.

  • $\begingroup$ This is nice! Is there a reference? $\endgroup$ Apr 5, 2015 at 19:51
  • 2
    $\begingroup$ I just cooked it up so I don't know, but it looks easy enough for someone to have observed it earlier. My inspiration was the argument that topological sorting of partial orders can be done in TC^0, hence t.s. of acyclic graphs in NL; this positively has a reference, but I'm not at the office at the moment, so it's difficult for me to look for it. $\endgroup$ Apr 5, 2015 at 20:51
  • 1
    $\begingroup$ The result that satisfying assignments can be computed in FNL appears with a different argument in Cook, Kolokolova: A second-order theory for NL, and with a bit more details in Cook, Nguyen: Logical foundations of proof complexity. However, I confess I can’t figure out how it is supposed to work. As far as I can tell, property (307) left as an exercise for the reader in the C&N book is simply false. $\endgroup$ Apr 6, 2015 at 14:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.