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