The 2CNF Boolean Formula Satisfiability Problem and the Linear Space Hypothesis
share
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--the 2CNF Boolean formula satisfiability problem--parameterized by the number of Boolean variables. It is shown that 2SAT with n variables and m clauses can be solved simultaneously polynomial time and n/2^c√(logn) 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 as literals in at most 3 clauses--cannot be solved simultaneously in polynomial time using strictly "sub-linear" (i.e., n^e polylog(n) for a certain constant e in (0,1)) space. An immediate consequence of this working hypothesis is L=/=NL. Moreover, we use our hypothesis as a plausible basis to lead to the insolvability of various NL search problems as well as the nonapproximability of NL optimization problems. For our investigation, since standard logarithmic-space reductions may no longer preserve polynomial-time sub-linear-space complexity, we need to introduce a new, practical notion of "short reduction." It turns out that the complement of 2SAT_3 is complete for a restricted version of NL, called Syntactic NL or simply SNL, under such short reductions. This fact supports the legitimacy of our working hypothesis.
READ FULL TEXT