The 2CNF Boolean Formula Satisfiability Problem and the Linear Space Hypothesis

We aim at investigating the solvability/insolvability of nondeterministic logarithmic-space (NL) decision, search, and optimization problems parameterized by size parameters using simultaneously polynomial time and sub-linear space on multi-tape deterministic Turing machines. We are particularly focused on a special NL-complete problem, 2SAT parameterized by the total number $m_{vbl}(\phi)$ of Boolean variables of each given Boolean formula $\phi$. It is shown that 2SAT with $n$ variables and $m$ clauses can be solved simultaneously polynomial time and $(n/2^{c\sqrt{\log{n}}})\, polylog(m+n)$ space for an absolute constant $c>0$. This fact inspires us to propose a new, practical working hypothesis, called the linear space hypothesis (LSH), which states that 2SAT$_3$ -- a restricted variant of 2SAT in which each variable of a given 2CNF formula appears at most 3 times in the form of literals -- cannot be solved simultaneously in polynomial time using strictly ``sub-linear'' (i.e., $m_{vbl}(x)^{\varepsilon}\, polylog(|x|)$ for a certain fixed constant $\varepsilon\in[0,1)$) space on all instances $x$. Immediate consequences of this working hypothesis include $\mathrm{L}\neq\mathrm{NL}$, $\mathrm{LOGDCFL}\neq\mathrm{LOGCFL}$, and $\mathrm{SC}\neq \mathrm{NSC}$. For our investigation, since standard logarithmic-space reductions may no longer preserve polynomial-time sub-linear-space complexity, we need to introduce a new, restricted notion of ``short reduction.'' For a syntactically restricted version of NL, called Syntactic NL$_{\omega}$ or SNL$_{\omega}$, $(\mathrm{2SAT}_3,m_{vbl})$ is in fact hard for parameterized SNL$_{\omega}$ via such short reductions. This fact supports the legitimacy of our working hypothesis.