2-संतुष्टि (2-सैट) सी/सी++ में समस्या?

मान लीजिए f =(x1 ∨ y1) ∧ (x2 ∨ y2) ∧ ... ∧ (xn yn)।

समस्या:क्या f संतोषजनक है?

xi यी और और

सभी समकक्ष हैं। इसलिए हम प्रत्येक (xi yi) s को उन दो कथनों में परिवर्तित कर रहे हैं।

अब 2n शीर्षों वाला एक आलेख मानिए। प्रत्येक (xi∨yi) के मामले में दो निर्देशित किनारों को जोड़ा जाता है

• xi से यी तक

• yi से xi तक

f को संतोषजनक नहीं माना जाता है यदि xi और xi दोनों एक ही SCC (स्ट्रॉन्गली कनेक्टेड कंपोनेंट) में हों

मान लें कि 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