সমস্যা বিবরণ
f = (x1 ∨ y1) ∧ (x2 ∨ y2) ∧ ... ∧ (xn ∨ yn) দেওয়া আছে। f স্যাটিসফাইয়েবল কিনা তা বের করতে হবে।
xi ∨ yi, ¬xi → yi এবং ¬yi → xi সমতুল্য। তাই প্রতিটি (xi ∨ yi) কে দুটি ডিরেক্টেড এজে রূপান্তর করা হয়।
২n ভার্টেক্স বিশিষ্ট একটি গ্রাফ ধরা হয়। প্রতিটি (xi ∨ yi)-র জন্য দুটি ডিরেক্টেড এজ:
- ¬xi থেকে yi
- ¬yi থেকে xi
যদি f স্যাটিসফাইয়েবল হয়, তবে টপোলজিক্যাল সোর্ট দিয়ে ভেরিয়েবলগুলোর মান অ্যাসাইন করা যায়। ¬xi, xi-র পরে টপোলজিক্যাল সোর্টে থাকলে xi = FALSE, অন্যথায় TRUE।
সিউডো কোড
func dfsFirst(vertex v):
marked[v] = true
for each u adjacent to v:
if not marked[u]: dfsFirst(u)
stack.push(v)
func dfsSecond(vertex v):
marked[v] = true
for each u adjacent to v:
if not marked[u]: dfsSecond(u)
component[v] = counter
for i = 1 to n:
addEdge(not x[i], y[i])
addEdge(not y[i], x[i])
for i = 1 to n:
if not marked[x[i]]: dfsFirst(x[i])
if not marked[y[i]]: dfsFirst(y[i])
if not marked[not x[i]]: dfsFirst(not x[i])
if not marked[not y[i]]: dfsFirst(not y[i])
set all marked false
counter = 0
flip directions of edges
while stack not empty:
v = stack.pop
if not marked[v]:
counter = counter + 1
dfsSecond(v)
for i = 1 to n:
if component[x[i]] == component[not x[i]]: unsatisfiable; exit
if component[y[i]] == component[not y[i]]: unsatisfiable; exit
satisfiable; exit
