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 次瀏覽

開啟你的 職業生涯

完成課程，獲得認證

立即開始
廣告