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.

翻译：我们旨在研究由规模参数参数化的非确定性对数空间（NL）的判定、搜索和优化问题在多带确定性图灵机上同时使用多项式时间和亚线性空间的可解性/不可解性。我们特别关注一个特殊的NL完全问题——2SAT，该问题由每个给定布尔公式φ的布尔变量总数m_{vbl}(φ)参数化。结果表明，对于绝对常数c>0，具有n个变量和m个子句的2SAT可以在多项式时间及(n/2^{c√log n})·polylog(m+n)空间内同时求解。这一事实启发我们提出一个新的、实用的工作假设，称为线性空间假设（LSH），即2SAT₃（2SAT的一个受限变体，其中给定2CNF公式的每个变量以文字形式最多出现3次）无法在所有实例x上同时使用严格“亚线性”（即对于某个固定常数ε∈[0,1)，空间为m_{vbl}(x)^ε·polylog(|x|)）空间的多项式时间求解。该工作假设的直接推论包括L≠NL、LOGDCFL≠LOGCFL以及SC≠NSC。在我们的研究中，由于标准对数空间归约可能不再保持多项式时间亚线性空间复杂度，我们需要引入一种新的受限归约概念——“短归约”。对于NL的一个语法受限版本，称为语法NLω（SNLω），(2SAT₃, m_{vbl})实际上通过此类短归约对参数化SNLω是困难的。这一事实支持了我们的工作假设的合理性。