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

2022-05-15 19:19:35 字數 2536 閱讀 4041

(點選此處檢視原題)

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 問題 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 的...