(點選此處檢視原題)
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#includeview code#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;
}
模板 2 SAT 問題 2 SAT
2 sat 問題 模板 有n個布林變數 x 1 x n 另有m個需要滿足的條件,每個條件的形式都是 x i 為true false或 x j 為true false 比如 x 1 為真或 x 3 為假 x 7 為假或 x 2 為假 2 sat 問題的目標是給每個變數賦值使得所有條件得到滿足。輸入格式...
模板 2 SAT 問題
2 sat問題主要解決的是一類二取一的問題.做法就是先建圖,然後跑tarjan,然後就判斷正負是否衝突,假如有衝突,就說明無解,否則就判斷哪個的序號大.話說我也不知道為什麼序號大就代表1.題幹 題目背景 2 sat 問題 模板 題目描述 有n個布林變數x1x 1x1 xnx nxn 另有m個需要滿足...
P4782 模板 2 SAT 問題
傳送門 2 sat的板子 把每乙個點拆成選0或選1 條件為 x i 為 a 或 x j 為 b 那麼如果 x i 不為 a 則 x j 必為 b 同理 x j 不為 b 則 x i 必為 a 那麼從 x i 不為 a 的點向 x j 為 b 的點連邊,從 x j 不為 b 的點向 x i 為 a 的...