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

TL;DR

This paper introduces the linear space hypothesis (LSH), a new conjecture about the complexity of solving a restricted 2SAT problem within sub-linear space, with implications for fundamental complexity class separations.

Contribution

It proposes the LSH, linking the complexity of 2SAT_3 with major class separations, and explores the properties of short reductions in parameterized complexity.

Findings

LSH implies L ≠ NL and other class separations.

Full utilization of short reductions shows PsubLIN class closure.

Provides a new perspective on space-bounded complexity of 2SAT variants.

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}(\phi)$ of variables of each given Boolean formula $\phi$. 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.