带有两个子句的 SAT 是多项式答案

【问题标题】：SAT with two clauses is polynomial带有两个子句的 SAT 是多项式
【发布时间】：2015-07-27 13:56:12
【问题描述】：

具有 k 个一元子句且只有两个子句的 SAT 实例的复杂性是多少？

我想找一篇有这个结果的论文。我找到了一篇问题有点不同的论文。所有变量最多出现两次...

【问题讨论】：

如果您的问题的答案不正确，请随时评论。或者，通过选择答案将问题标记为已解决。

标签： polynomial-math np-complete clause propagation sat

【解决方案1】：

如果我理解正确，这似乎是从句总长度中的线性时间。

一元从句立即强制部分变量赋值 τ。如果两个子句中的任何一个在 τ 下不可满足（空），或者某些单元子句相互冲突，则该实例是不可满足的。否则，仅当两个子句在 τ 下是单位且互补的，即 x̅ 和 x 时，该实例才不可满足。

【讨论】：

【解决方案2】：

您的问题有一个complexity in O(n)，其中n is the total size of clauses。

你有K个一元子句，这些K个一元子句可以看作是变量的子赋值。如果你不尊重这些一元从句，你肯定找不到解决方案（如果存在的话）。

让我们举个例子来看看你的问题，目标是找到variables的值。

 variables = _ _ _ _ _ _ _ _
 problem   = 
              x1                 AND
              x4                 AND
              x7                 AND
             -x8                 AND
             -x5                 AND
              x2                 AND
              x3 OR  -x4 OR x5   AND
              x6 OR  -x1 OR x8

 with K = 5.

因为一元子句会将它们的值传播到variables，所以这个问题基本上是一样的：

 variables = x1 x2 _ x4 -x5 _ x7 -x8
 problem   = 
              x3 OR  -x4 OR  x5  AND
              x6 OR  -x1 OR  x8
 with K = 0.

（为了得到这个，我们做了一个线性时间操作）。

因为，我们已经知道 x4、x5、x1 和 x8 的值，所以这个问题与：

 variables = x1 x2 _ x4 -x5 _ x7 -x8
 problem   = 
              x3 AND
              x6
 with K = 0.

（为了获得这个，我们再次进行了线性时间操作）。

通过调用与第一个操作相同的函数，我们将获得：

 variables = x1 x2 x3 x4 -x5 x6 x7 -x8
 problem   = 
              true.
 with K = 0.

（我们再次进行了线性时间运算来得出这个结论）。

哪个给你最终的解决方案：variables = x1 x2 x3 x4 -x5 x6 x7 -x8 如您所见，要找到解决方案只能通过使用线性时间运算来完成。

【讨论】：