2 SAT問題介紹求解模板題P4782

（點選此處檢視原題）

sat 即 satisfiability，意思為可滿足，那麼2-sat表示一些布林變數只能取true或者false，而某兩個變數之間的值存在一定的關係（如：只要a為真，b一定為假；如果a為假，b也為假），我們需要在滿足所有這樣的關係的情況下，求出每個變數的賦值，如果不存在，就是無解。

某一天，pc，yd，hl在討論兩個問題：1）winter的溫度是否低於0度，2）bamboo的高度是否大於10m，眾所周知，這三位大佬很強大，所以他們對於這兩個問題的判斷至少有乙個是正確的。此時給出三人對這兩個問題的判斷，求出這兩個問題的正確答案；如果不存在正確答案，那麼可能是某個人犯糊塗了，因此我們無法得到答案，輸出無解。

我們將兩個問題符號化為，a：winter的溫度低於0度， b ：bamboo的高度大於10m，將三人的觀點及其符號化表示如下：

1）pc認為：winter的溫度低於0度，bamboo的高度大於10m，a∨ b

2）yd認為：wintet的溫度不低於0度，bamboo的高度大於10m，¬a∨ b

3）hl認為：winter的溫度不低於0度，bamboo的高度不大於10m，¬a∨ ¬b

那麼a,b的取值需要滿足：(a∨ b) ∧ ( ¬a∨ b) ∧ (¬a∨ ¬b)，我們如何求出滿足這個式子的a,b的取值這類問題就是2-sat問題。

我們可以將每個變數x的兩個狀態分別用兩個點表示，記編號為i的點表示這個變數取真，i+n的點表示這個變數取假

將兩個變數之間的關係用邊表示，如：只要a為真，b一定為假，將此命題符號化得到¬a∨¬

b，這個式子也可以寫成：

a → ¬b ∧ b → ¬a，表示：a為真，則b必為假，和b為真，則a必為假，這樣我們就發現 a 和 ¬b 可以由a推出¬b，可以由b推出¬a，在圖中，我們構建這樣的邊表示他們的關係：由 a 向 ¬b 建一條單向邊，再由 b 向 ¬a建一條單向邊，總結以下將命題轉化為建圖的規律：

1）¬a∨¬b ----> a → ¬b ∧ b → ¬a

2）a∨b ----> ¬a → b ∧ ¬b → a

3）¬a∨b ----> a → b ∧ ¬b → ¬a

4）a∨¬b ----> ¬a → ¬b ∧ b → a

(x→y可以視作由x向y建一條單向邊）

然後，我們在這個圖中求強連通分量，聯想到我們圖中邊代表的關係：由邊的起點可以推出終點，所以同一強連通分量中的點真值一致，所以我們很容易想到如果 a 和 ¬a在同一強連通分量中，這說明a和¬a真值相同，這顯然是不正確的，即無解；如果不存在變數x使得x和¬x在同一強連通分量中，就說明有解。

那麼有解的情況下，我們如何得到每個變數的值呢？只要x所在強連通分量的拓撲序比¬x所在強連通分量的拓撲序靠後，則x為真，否則為假，而我們用tarjan演算法求強連通分量的時候，對於每個強連通分量的標記是逆拓撲序的，所以 node[x] < node[¬x] 時，x取真，否則為假，這樣一來，我們對每個變數進行判斷並輸出對應的值即可

#include#include
#include
#include
#include
#include
#include
#include
#include
#include 
#include 
#define bug cout << "**********" << endl
#define show(x, y) cout<
using
namespace
std;
typedef 
long
long
ll;const ll inf = 2e9 + 10
;const ll mod = 1e9 + 7
;const
int max = 2e6 + 10
;const
int max2 = 3e2 + 10
;struct
egde
edge[max];
intn, m;
inthead[max], tot;
intdfn[max], low[max],time_clock;
intline[max],now;
intnode[max],scccnt;
void
init()
void add(int u, int
v)void tarjan(int
u)        
else
if(!node[v])
}if(dfn[u] ==low[u])
}int
main()
for(int i = 1;i <= (n << 1) ;i ++)
bool ok = true
;        
for(int i = 1;i <= n ;i ++)
}if(!ok)
else
printf(
"%d\n
",node[n] < node[n<<1
]);        }
}return0;
}

view code

2 SAT問題介紹求解模板題P4782

模板 2 SAT 問題 2 SAT

模板 2 SAT 問題

P4782 模板 2 SAT 問題

2 SAT問題介紹求解 模板題P4782

模板 2 SAT 問題 2 SAT

模板 2 SAT 問題

P4782 模板 2 SAT 問題

相關推薦

2 SAT問題介紹求解模板題P4782