C/C++ 中的 2-可满足性 (2-SAT) 问题？

设 f = (x1 ∨ y1) ∧ (x2 ∨ y2) ∧ ... ∧ (xn ∨ yn)。

问题：f 可以满足吗？

xi ∨ yi 和 和 

 是等价的。所以我们将每个 (xi ∨ yi) 转换成这两条语句。

现在假设有一个 2n 个顶点的图。对于每个 (xi∨yi)，添加两条有向边

  • 从 ¬xi 到 yi

  • 从 ¬yi 到 xi

如果 ¬xi 和 xi 都在同一个 SCC（强连通分量）中，则 f 将不会被视为可满足的

假设 f 被视为可满足的。现在我们要为每个变量提供值以满足 f。可以使用我们构造的图的顶点拓扑排序来执行此操作。如果 ¬xi 在拓扑排序中排在 xi 之后，则 xi 应视为 FALSE。否则应将其视为 TRUE。

伪代码

func dfsFirst1(vertex v1):
   marked1[v1] = true
   for each vertex u1 adjacent to v1 do:
      if not marked1[u1]:
            dfsFirst1(u1)
      stack.push(v1)
   func dfsSecond1(vertex v1):
      marked1[v1] = true
      for each vertex u1 adjacent to v1 do:
         if not marked1[u1]:
            dfsSecond1(u1)
   component1[v1] = counter
for i = 1 to n1 do:
      addEdge1(not x[i], y[i])
      addEdge1(not y[i], x[i])
for i = 1 to n1 do:
   if not marked1[x[i]]:
      dfsFirst1(x[i])
   if not marked1[y[i]]:
      dfsFirst1(y[i])
   if not marked1[not x[i]]:
      dfsFirst1(not x[i])
   if not marked1[not y[i]]:
      dfsFirst1(not y[i])
set all marked values false
counter = 0
flip directions of edges // change v1 -> u1 to u1 -> v1
while stack is not empty do:
   v1 = stack.pop
   if not marked1[v1]
      counter = counter + 1
      dfsSecond1(v1)
for i = 1 to n1 do:
   if component1[x[i]] == component1[not x[i]]:
      it is unsatisfiable
      exit
   if component1[y[i]] == component1[not y[i]]:
      it is unsatisfiable
      exit
it is satisfiable
exit

更新时间：2020 年 1 月 29 日

269 次浏览

开启你的 职业生涯

完成课程，获得认证

立即开始
广告