（本文可能需要一點
離散數學
基礎）
SAT
，即布林可滿足性問題，是判定一個
命題公式
是否為
可滿足式
［1］
的問題。這個問題被證明是
NP-完全
的（相關科普可參考這篇知乎文章），目前沒有多項式時間內的解法。
我們轉而考慮SAT的簡單版本，即命題公式為
合取正規化
［2］
，且組成它的每個
簡單析取式
［2］
都至多含有
個
文字
［2］
，這一問題稱為
n-SAT
。當
時，n-SAT也已被證明是NP-完全問題，幸運的是，
時，這個問題有多項式時間的解法。
我們把2-SAT轉化為
圖論
問題。假設原命題公式有
共
個命題變元，便一共有
種可能的文字，對於每個文字，我們都用一個點表示。設
與
均為文字，如果
為真，則
和
均為真（其中
為
蘊含
），於是從
往
連一條有向邊，從
往
連一條有向邊。
注意根據蘊含的性質，如果
為真，則
為真，所以在我們建出的圖中，
可達
意味著原公式可滿足時，
應該為真。我們對每個命題變元進行如下考察：
如果
可達
，則
即
即
應為真，或者說
應為假
如果
可達
，則
即
即
應為真
如果
與
相互可達，那原命題公式是矛盾式
如果
與
相互不可達，那
可以任意賦值
這當然可以用傳遞閉包
地解決，但是還有更快的方法。我們先求一下強連通分量，如果某個
和
屬於同一個強連通分量，那它們互相可達，肯定是矛盾式。然後對比
和
（在縮點得到的DAG上）的拓撲序，把拓撲序較大的一個點設為真，因為如果它們之間單連通則一定是拓撲序較小的點可達拓撲序較大的點，如果它們之間不連通則怎樣賦值都無所謂。因為Tarjan演算法求強連通分量的過程中已經得到了拓撲序，我們不需要額外進行拓撲排序。複雜度是
。
具體實現時，可以用
號點表示
，
號點表示
。這樣要求
的對應點
的編號只需要異或上1。
以下是洛谷模板題的主要程式碼：
int
n
，
m
；
cin
>>
n
>>
m
；
while
（
m
——
）
{
int
i
，
a
，
j
，
b
；
cin
>>
i
>>
a
>>
j
>>
b
；
edges
［（
2
*
i
+
a
）
^
1
］。
push_back
（
2
*
j
+
b
）；
edges
［（
2
*
j
+
b
）
^
1
］。
push_back
（
2
*
i
+
a
）；
}
for
（
int
i
=
2
；
i
<=
n
*
2
+
1
；
++
i
）
if
（
！
dfsn
［
i
］）
tarjan
（
i
）；
for
（
int
i
=
1
；
i
<=
n
；
++
i
）
{
if
（
scc
［
i
*
2
］
==
scc
［
i
*
2
+
1
］）
return
cout
<<
“IMPOSSIBLE”
<<
endl
，
0
；
else
if
（
scc
［
i
*
2
］
>
scc
［
i
*
2
+
1
］）
ans
［
i
］
=
1
；
else
ans
［
i
］
=
0
；
}
cout
<<
“POSSIBLE”
<<
endl
；
for
（
int
i
=
1
；
i
<=
n
；
++
i
）
cout
<<
ans
［
i
］
<<
“ ”
；
參考
^
對於某個命題公式，如果存在一組賦值使它為真，則稱它為可滿足式；否則為矛盾式。
^
a
b
c
命題變元或其否定稱為文字。若干個文字的析取稱為簡單析取式，例如a∨¬b∨c。簡單析取式的合取稱為合取正規化，例如（¬a∨c）∧b∧（a∨¬b∨c）。
