Consider a 3SAT instance with the following special locality property. Suppose there are n variables in the Boolean formula, and that they are numbered 1,2,3....n in such a way that each clause involves variables whose numbers are within +-10 of each other. Give a linear-time algorithm for solving such an instance of 3SAT.
I could not solve the problem but my intuition is that if we could map the problem in graph then may be solved but could not go much farther ..
This is a relatively straightforward dynamic programming problem. I'll describe a solution, ignoring the fairly straightforward indexing issues around either boundary.
After the m'th step we have the set of possible values for variables (m-10, m-9, ..., m+10) which could be solutions so far, each linked to a set of values for all previous variables that leads to solutions to equations 1..m.
For the m+1'th step we take each member of this possible solution set, ignore the m-10'th value, and consider each possibility for the m+11'th value. If the m+1'th equation is true, we add this to the next solution set, pointing to our history, only if that solution pattern has not already been added.
This lands us ready for the m+2nd step.
There are n steps required, each of which can have about 2 million possible cases to consider, so this is linear.
(Fun challenge. Modify this algorithm to not just find a solution, but to count how many solutions there are.)
I think you can just brute force it in poly time. Divide the clause list into two pieces. Exhaustive search over variables which are on both sides of the split. There are at most 30 of them, so that's 2^30 = O(1) settings to try. Once those variables are set, you can recursively solve both sides, each one is an independent SAT instance with n/2 variables.
