È una versione "locale" di NP-Hard a 3-Sat?

Question

Di seguito è la mia semplificazione di una parte di un progetto di ricerca più ampio sulle reti bayesiane spaziali:

Dire una variabile è "$ k $-local "in una stringa $ C in 3 text {-cnf} $ Se ce ne sono meno di $ k $ clausole tra la prima e l'ultima clausola in cui appare (dove $ k $ è un numero naturale).

Ora considera il sottoinsieme $ (3, k) text {-lsat} sottoseteq 3 text {-sat} $ definito dal criterio che per qualsiasi $ C in (3, k) text {-lsat} $, ogni variabile in $ C $ è $ k $-Locale. Per quello $ k $ (se presente) è $ (3, k) text {-lsat} $ NP-Hard?

---

Ecco cosa ho considerato finora:

(1) Variazioni sul metodo di dimostrarlo $ 2 text {-sat} $ è in p riscrivendo ogni disgiunzione come implicazione ed esaminando i percorsi diretti sul grafico diretto di queste implicazioni (notato qui e presentato in dettaglio alle pagine 184-185 di Papadimitriou Complessità computazionale). A differenza di $ 2 text {-sat} $, c'è una ramificazione dei percorsi diretti in $ (3, k) text {-lsat} $, ma forse il numero di percorsi diretti è limitato dai vincoli spaziali sulle variabili. Finora nessun successo con questo.

(2) una riduzione del tempo polinomiale di $ 3 text {-sat} $ (o altro problema NP-completo noto) a $ (3, k) text {-lsat} $. Ad esempio, ho provato vari schemi di introduzione di nuove variabili. Tuttavia, riunendo le clausole che contengono la variabile originale $ x_k $ Generalmente richiede che io trascino "catene" di clausole aggiuntive contenenti le nuove variabili e queste interferiscono con i vincoli spaziali sulle altre variabili.

Sicuramente non sono in un nuovo territorio qui. C'è un problema noto np-hard a cui può essere ridotto $ (3, k) text {-lsat} $ O i vincoli spaziali impediscono il problema di essere così difficile?