- sat search-problem logspace
- Updated Fri, 20 May 2022 17:58:32 GMT

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)?

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$.

- +0 – This is nice! Is there a reference? — Apr 05, 2015 at 19:51
- +2 – 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. — Apr 05, 2015 at 20:51
- +1 – 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 cant 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. — Apr 06, 2015 at 14:55

External links referenced by this document: