ให้ f =(x1 ∨ y1) ∧ (x2 ∨ y2) ∧ ... ∧ (xn ∨ yn)
ปัญหา:พอใจไหม
ซี ∨ ยี่ และ 
และ 
มีค่าเท่ากันทั้งหมด ดังนั้นเราจึงแปลง (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
