2-C / C ++の満足度（2-SAT）の問題？

f =（x1∨y1）∧（x2∨y2）∧...∧（xn∨yn）とします。

問題：fは満足できるか？

xi∨yiと および

すべて同等です。したがって、（xi∨yi）のそれぞれをこれらの2つのステートメントに変換しています。

ここで、2n個の頂点を持つグラフを想定します。 （xi∨yi）のそれぞれの場合、2つの有向エッジが追加されます

• ¬xiからyiへ

• ¬yiからxiへ

¬xiとxiの両方が同じSCC（Strongly Connected Component）にある場合、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