Are there any hard instances of 3-SAT when the clauses can only use literals that are "nearby" each other?

Question

Let the variables be $x_1 , x_2 , x_3 ... x_n$. The distance between two variables is defined as $d(x_a , x_b) = |a-b|$. The distance between two literals is the distance between the corresponding two variables.

Suppose I have a 3-SAT instance such that for every clause $(x_a , x_b, x_c)$ we have $d(x_a , x_b) \leq N \wedge d(x_a , x_c) \leq N \wedge d(x_b , x_c) \leq N$ for some fixed value $N$.

Conceptually you can picture this as all the literals being physically on a line and all the clauses are incapable of reaching beyond a certain length for physical reasons.

Given this constraint are there any hard instances of 3-SAT? How small can I make the neighborhood and still find hard instances? What if I allow a few clauses to violate the constraint?

By hard I mean a heuristic solver would fall back on the worst case.

Answer 1

No. If the 3-SAT instance has $m$ clauses, then you can test satisfiability in $O(m 2^N)$ time. Since $N$ is a fixed constant, this is a polynomial-time algorithm that solves all instances of your problem.

The algorithm works in $m$ stages. Let $\varphi_i$ denote the formula consisting of the clauses that use only variables from $x_1,\dots,x_i$. Let $S_i \subseteq \{0,1\}^n$ denote the set of assignments to $x_{i-N},x_{i-N+1},\dots,x_i$ that can be extended to a satisfying assignment for $\varphi_i$. Note that given $S_{i-1}$, we can compute $S_i$ in $O(2^N)$ time: for each $(x_{i-N-1},\dots,x_{i-1}) \in S_{i-1}$, we try both possibilities for $x_i$ and check whether it satisfies all clauses from $\varphi_i$ that contain the variable $x_i$; if so, we add $(x_{i-N},\dots,x_{i})$ to $S_i$. In the $i$th stage, we compute $S_i$. Once we have finished all $m$ stages, the 3-SAT instance is satisfiable if and only if $S_m \ne \emptyset$. Each stage takes $O(2^N)$ time, and there are $m$ stages, so the total running time is $O(m 2^N)$. This is polynomial in the size of the input, and thus constitutes a polynomial-time algorithm.

Even if you allow a fixed number of clauses to violate the constraint, the problem can still be solved in polynomial time. In particular, if $t$ counts the number of clauses that violate the constraint, you can solve the problem in $O(m 2^{(t+1)N})$ time, by first enumerating all possible values for the variables in those clauses, then continuing with the algorithm above. When $t$ is a fixed constant, this is polynomial time. There may be more efficient algorithms.

Answer 2

Incident graph of a SAT formula is a bipartite graph that has a vertex for each clause and each variable. We add edges between a clause and all of its variables. If the incident graph has bounded treewidth then we can decide the SAT formula in P, actually we can do much more. Your incident graph is very restricted. E.g it is a bounded pathwidth graph, so it is polynomial time solvable. For the above well known structural result e.g. take a look at: https://www.sciencedirect.com/science/article/pii/S0166218X07004106.