C/C++의 2-만족도(2-SAT) 문제?

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

문제:f가 만족스러운가?

xi ∨ 이 및 및

모두 동등합니다. 그래서 우리는 각각의 (xi ∨ yi) 를 이 두 문장으로 변환합니다.

이제 2n개의 꼭짓점이 있는 그래프를 가정합니다. (xi∨yi) 각각의 경우 두 방향 모서리가 추가됩니다.

• ¬xi에서 yi까지

• ¬yi에서 xi까지

f는 ¬xi와 xi가 모두 동일한 SCC(Strongly Connected Component)에 있는 경우 만족스러운 것으로 처리되지 않습니다.

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