The 2CNF Boolean Formula Satisfiability Problem and the Linear Space Hypothesis
Tomoyuki Yamakami
TL;DR
The paper introduces the Linear Space Hypothesis (LSH) for 2SAT$_3$, positing that no deterministic polynomial-time algorithm can solve $(2\mathrm{SAT}_3,m_{vbl})$ using sub-linear space $m_{vbl}(x)^{\varepsilon}\mathrm{polylog}(|x|)$ for any $\varepsilon\in[0,1)$. It develops a framework of short reductions and PsubLIN to study polynomial-time sub-linear-space solvability and proves equivalences: LSH(2SAT$_3$) is equivalent to LSH for LP$_{2,3}$ and for 3DSTCON, and to multiple variants with $m_{cls}$, expanding the landscape of hardness assumptions beyond standard P vs NP. The work shows that LSH implies strong separations such as $\mathrm{L}\neq\mathrm{NL}$ and $\mathrm{LOGDCFL}\neq\mathrm{LOGCFL}$, and it derives concrete applications to NL search/optimization and automata theory, including non-solvability results for Search-1NFA and Search-UOCK, non-approximation results for Max-HPP, and hardness of transforming unary 1NFAs to 1DFAs. By linking 2SAT$_3$ to structural NL frameworks (SNL, para-SNL$_{\omega}$) and to well-studied problems (LP$_{2,3}$, DSTCON), the paper provides accessible targets for proving space-based lower bounds with broad implications for sub-linear-space computation. Significantly, LSH offers a practical, testable conjecture driving research into more refined lower bounds and the complexity landscape of NL under resource-bounded regimes.
Abstract
We aim at investigating the solvability/insolvability of nondeterministic logarithmic-space (NL) decision, search, and optimization problems parameterized by natural size parameters using simultaneously polynomial time and sub-linear space. We are particularly focused on $\mathrm{2SAT}_3$ -- a restricted variant of the 2CNF Boolean (propositional) formula satisfiability problem in which each variable of a given 2CNF formula appears at most 3 times in the form of literals -- parameterized by the total number $m_{vbl}(φ)$ of variables of each given Boolean formula $φ$. We propose a new, practical working hypothesis, called the linear space hypothesis (LSH), which asserts that $(\mathrm{2SAT}_3,m_{vbl})$ cannot be solved in polynomial time using only ``sub-linear'' space (i.e., $m_{vbl}(x)^{\varepsilon}\, polylog(|x|)$ space for a constant $\varepsilon\in[0,1)$) on all instances $x$. Immediate consequences of LSH include $\mathrm{L}l\neq\mathrm{NL}$, $\mathrm{LOGDCFL}\neq\mathrm{LOGCFL}$, and $\mathrm{SC}\neq \mathrm{NSC}$. For our investigation, we fully utilize a key notion of ``short reductions'', under which the class $\mathrm{PsubLIN}$ of all parameterized polynomial-time sub-linear-space solvable problems is indeed closed.