线性3SAT :线性时间的3SAT的一个版本

Question

考虑一个具有以下特殊locality属性的3SAT实例。假设布尔公式中有n个变量，并且它们的编号为1、2、3...n，这样每个子句都包含彼此编号在+-10内的变量。给出了求解这类3SAT问题的线性时间算法。

我不能解决这个问题，但我的直觉是，如果我们可以将问题映射到图中，那么问题可能会得到解决，但不能走得更远。

Answer 1

这是一个相对简单的动态编程问题。我将描述一种解决方案，忽略任何边界周围相当简单的索引问题。

在第m步之后，我们得到了变量(m-10，m-9，...，m+10)的可能值的集合，这些值可能是到目前为止的解，每个值都链接到所有先前变量的一组值，这些值导致方程1..m的解。

对于第m+1步，我们取这个可能解集的每个成员，忽略第m-10‘个值，并考虑第m+11’个值的每种可能性。如果第m+1‘个方程为真，我们将其添加到下一个解决方案集中，指向我们的历史，只有在尚未添加该解决方案模式的情况下。

这使我们为m+2nd步骤做好了准备。

需要n个步骤，每个步骤可以考虑大约200万个可能的情况，所以这是线性的。

有趣的挑战。修改此算法，不仅可以找到解决方案，还可以计算有多少个解决方案。)

Answer 2

我想你可以在短时间内暴力破解它。将子句列表分成两部分。对分裂两侧的变量进行详尽的搜索。它们最多有30个，所以可以尝试2^30 = O(1)个设置。一旦设置了这些变量，您就可以递归地求解两边，每个变量都是一个具有n/2个变量的独立SAT实例。