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?