Is a "local" version of 3-SAT NP-hard?

Below is my simplification of part of a larger research project on spatial Bayesian networks:

Say a variable is "$k$-local" in a string $C \in 3\text{-CNF}$ if there are fewer than $k$ clauses between the first and last clause in which it appears (where $k$ is a natural number).

Now consider the subset $(3,k)\text{-LSAT} \subseteq 3\text{-SAT}$ defined by the criterion that for any $C \in (3,k)\text{-LSAT}$, every variable in $C$ is $k$-local. For what $k$ (if any) is $(3,k)\text{-LSAT}$ NP-hard?

Here is what I have considered so far:

(1) Variations on the method of showing that $2\text{-SAT}$ is in P by rewriting each disjunction as an implication and examining directed paths on the directed graph of these implications (noted here and presented in detail on pp. 184-185 of Papadimitriou's Computational Complexity). Unlike in $2\text{-SAT}$, there is branching of the directed paths in $(3,k)\text{-LSAT}$, but perhaps the number of directed paths is limited by the spatial constraints on the variables. No success with this so far though.

(2) A polynomial-time reduction of $3\text{-SAT}$ (or other known NP-complete problem) to $(3,k)\text{-LSAT}$. For example, I've tried various schemes of introducing new variables. However, bringing together the clauses that contain the original variable $x_k$ generally requires that I drag around "chains" of additional clauses containing the new variables and these interfere with the spatial constraints on the other variables.

Surely I'm not in new territory here. Is there a known NP-hard problem that can be reduced to $(3,k)\text{-LSAT}$ or do the spatial constraints prevent the problem from being that difficult?

$(3,k)\text{-LSAT}$ is in P for all $k$. As you have indicated, locality is a big obstruction to NP-completeness.

Here is a polynomial algorithm.

Input: $\phi\in (3,k)\text{-LSAT}$, $\phi=c_1\wedge c_2\cdots \wedge c_m$, where $c_i$ is the $i$-th clause.

Output: true if $\phi$ becomes 1 under some assignment of all variables.

Procedure:

• Construct set $B_i$, the variables that appear in at least one of $c_i, c_{i+1}, \cdots, c_{i+k}$, $1\le i\le m-k$.

• Construct set $A_i=\{f: B_i\to\{0,1\} \mid c_i, c_{i+1}, \cdots, c_{i+k} \text{ become 1 under} f\}$.

• Construct set $E=\cup_i\{(f, g)\mid f\in A_i, g\in A_{i+1}, f(x)=g(x)\text{ for all }x\in B_i\cap B_{i+1} \}$

• Let $V=A_1\cup A_2\cdots\cup A_{m-k}$. Consider directed graph $G(V,E)$. For each vertex in $A_1$, start a depth-first search on $G$ to see if we can reach a vertex in $A_{m-k}$. If found, return true.

• If we have reached here, return false.

The correctness of the algorithm above comes from the following claim.

Claim. $\phi$ is satisfiable $\Longleftrightarrow$ there is a path in $G$ from a vertex in $A_1$ to a vertex in $A_{m-k}$.

Proof.

"$\Longrightarrow$": Suppose $\phi$ becomes 1 under assignment $f$. Let $f_i$ be the restriction of $f$ to $B_i$. Then we have a path $f_1, \cdots, f_{m-k}$.

"$\Longleftarrow$": Suppose there is a path $f_1, \cdots, f_{m-k}$, where $f_1\in A_1$ and $f_{m-k}\in A_{m-k}$. Define assignment $f$ such that $f$ agrees with all $f_i$, i.e., $f(x)=f_i(x)$ if $x\in B_i$. We can verify that $f$ is well-defined. Since $c_\ell$ becomes 1 for some $f_j$ for all $\ell$, $\phi$ becomes 1 under $f$.

The number of vertices $|V|\le 2^{3(k+1)}(m-k)$. Hence the algorithm runs in polynomial time in term of $m$, the number of clauses and $n$, the number of total variables.

StackExchange Computer Science Q#109357, answer score: 14