【发布时间】：2012-04-30 03:10:46
【问题描述】：
考虑具有以下特殊位置属性的 3SAT 实例。假设布尔公式中有 n 个变量，它们的编号为 1,2,3....n，这样每个子句都包含编号在 +-10 范围内的变量。给出求解此类 3SAT 实例的线性时间算法。
我无法解决问题，但我的直觉是，如果我们可以将问题映射到图表中，那么可能会解决但不能走得更远..
【问题讨论】：
标签： algorithm divide-and-conquer
【发布时间】：2012-04-30 03:10:46
【问题描述】：
我认为您可以在多时间内暴力破解它。将子句列表分成两部分。对拆分两侧的变量进行详尽搜索。最多有 30 个，因此可以尝试 2^30 = O(1) 设置。一旦设置了这些变量，您就可以递归求解两边，每一个都是具有 n/2 个变量的独立 SAT 实例。
【讨论】：
-
你能否详细说明为什么它是常数变量出现在分裂的两侧。
-
假设我们有类似 (x1 + x2'+ x3) | (x1' + x2 + x3) (x4'+ x5 + x6) | （x4 + x5' + x6）...................................... .......... (x30 + x31' + x32) | (x30 + x31 + x32') 那么分割的每一边都有30多个变量对吧！！！
-
我的意思是分裂的两边上出现的变量不超过30个。
-
假设我正在尝试创建一个问题的实例，其中有超过 30 个变量出现在拆分的两侧。让我们假设左侧
(x1 + x2 '+ x3) | (x1' + x2 + x3)
(x4'+ x5 + x6) | (x4 + x5' + x6)
......................
........ ....................
(x30 + x31' + x32) | (x30 + x31 + x32')
所以分裂的每一边都有超过 30 个共同的变量，也遵守对条款施加的条件..，可能我没有明白你的意思，请指出我的错误理解。问候 -
我不知道为什么断线不起作用我试图写的是有 | 是分割线所以双方总共包含 60 个子句我们可以将其增加到任意数量。
这是一个相对简单的动态规划问题。我将描述一个解决方案，忽略围绕任一边界的相当简单的索引问题。
在第 m 步之后，我们有一组可能的变量值 (m-10, m-9, ..., m+10)，它们可能是迄今为止的解决方案，每个都链接到一组值导致方程解的所有先前变量 1..m.
对于第 m+1' 步，我们采用这个可能的解决方案集的每个成员，忽略第 m-10' 值，并考虑第 m+11' 值的每种可能性。如果第 m+1 个方程为真，我们将其添加到下一个解决方案集中，指向我们的历史，前提是该解决方案模式尚未添加。
这让我们为第 m+2 步做好了准备。
需要 n 个步骤，每个步骤可以考虑大约 200 万个可能的情况，所以这是线性的。
（有趣的挑战。修改这个算法，不仅可以找到解决方案，还可以计算有多少解决方案。）
【讨论】：
-
是不是每一步我们都必须尝试使用 20 个变量，这反过来意味着要尝试 2^20 种可能的情况！！！我说的对吗？
-
如前所述，它实际上是 2^21（不要忘记 0）。尽管您实际上可以忽略第 m-10 个值以将其降低到 2^20。它是一个大常数，但它是一个常数，因此不会改变算法的大 O。