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.