2-sat學習筆記（補檔
重學2-sat
\(2-SAT\)是什麼
給定一個布林方程，判斷是否存在一組布林變數能滿足這個方程，方程的可行解被稱為\(SAT\)。這個問題是\(NP-hard\)的。但是如果我們對這個問題加上一些限制，就可以在多項式時間內求解了。設一個布林方程為：
\((a_1\lor a_2\cdots\lor a_n) \land (b_1\lor b_2\cdots\lor b_n) \cdots\)
如果一個布林方程滿足\(n<=2\),那麼這就是一個\(2-SAT\)問題。
如何表示\(2-SAT\)
因為每個布林變數只有兩種取值，所以我們可以將每個布林變數拆成兩個點後建圖。設將\(x\)
如果從\(a\)的值，我們能推出\(b\)的值。那我們就在圖中連一條有向邊。比如一個布林方程方程：\((a_1\lor a_2)\)，我們發現如果\(a_1\)為假，那麼\(a_2\)一定為真；同理如果\(a_2\)為假，那麼\(a_1\)一定為真。於是我們在圖中建兩條有向邊：\(a_1'->a_2\)和\(a_2'->a_1\)。這就是最基本的\(2-SAT\)建圖方法。
如何求解\(2-SAT\)
對於一個變數\(x\)，如果點\(x\)和點\(x'\)在同一個強連通分量中，那麼顯然這個布林方程無解，因為此時\(x\)
如果一個布林方程存在一組解，對於點\(x\)，如果\(x\)的拓撲序在\(x'\)之後，那麼答案就是\(x\)取真。反之，\(x\)就取假。因為這樣能夠避免衝突，構造出一組可行解
求解細節
先在圖中求一遍強連通分量。可以用\(kosaraj\)或者\(tarjan\)。注意\(kosaraju\)中強連通分量編號的順序就是該圖強連通分量的拓撲序。而在\(tarjan\)則是強聯通分量編號順序則和該圖強連通分量拓撲序相反。
程式碼
程式碼中強聯通分量用\(kosaraju\)求解
graph::kosaraju(); for (int i = 1; i <= n; ++i) { if (bel[i] == bel[i + n]) { puts("IMPOSSIBLE"); return 0; } } puts("POSSIBLE"); for (int i = 1; i <= n; ++i) { printf("%d ", bel[i] > bel[i + n]); }
例題
洛谷P4782
題意
求解\(2-SAT\)問題
題解
對每種情況分別連邊即可。設當前兩個變數分別為\(A\)和\(B\)
\(\begin{cases} A'->B, B'->A & A真B真\\ A'->B', B->A & A真B假 \\ A->B, B'->A' & A假B真 \\ A->B', B->A' & A假B假 \end{cases}\)
然後按照上面講的方法跑\(kosaraju\)求解即可。
// Author: 23forever
#include <bits/stdc++.h>
#define pb push_back
#define pii pair<int, int>
#define mp make_pair
#define fi first
#define se second
typedef long long LL;
const int MAXN = 2000000;
using namespace std;
inline int read() {
int x = 0, w = 1;
char c = ' ';
while (!isdigit(c)) {
c = getchar();
if (c == '-') w = -1;
}
while (isdigit(c)) {
x = (x << 1) + (x << 3) + (c ^ 48);
c = getchar();
}
return x * w;
}
int n, m, bel[MAXN + 5];
namespace graph {
const int MAXM = 4000000;
struct Edge {
int to, nxt;
Edge() {}
Edge(int _to, int _nxt) : to(_to), nxt(_nxt) {}
} edge[MAXM + 5], redge[MAXM + 5];
int tot, head[MAXN + 5], rtot, rhead[MAXN + 5];
inline void addEdge(int u, int v) {
edge[tot] = Edge(v, head[u]), head[u] = tot++;
redge[rtot] = Edge(u, rhead[v]), rhead[v] = rtot++;
}
inline void init() {
tot = 0, memset(head, -1, sizeof(head));
rtot = 0, memset(rhead, -1, sizeof(rhead));
}
vector < int > vec;
bool vis[MAXN + 5];
void dfs1(int u) {
vis[u] = true;
for (int i = head[u]; ~i; i = edge[i].nxt) {
int v = edge[i].to;
if (!vis[v]) dfs1(v);
}
vec.pb(u);
}
void dfs2(int u, int cnt) {
vis[u] = true;
bel[u] = cnt;
for (int i = rhead[u]; ~i; i = redge[i].nxt) {
int v = redge[i].to;
if (!vis[v]) dfs2(v, cnt);
}
}
void kosaraju() {
for (int i = 1; i <= 2 * n; ++i) {
if (!vis[i]) dfs1(i);
}
memset(vis, false, sizeof(vis));
int cnt = 0;
for (int i = vec.size() - 1; ~i; --i) {
if (!vis[vec[i]]) dfs2(vec[i], ++cnt);
}
}
}
void init() {
graph::init();
n = read(), m = read();
for (int t = 1; t <= m; ++t) {
int i = read(), a = read(), j = read(), b = read();
if (a && b) {
graph::addEdge(i + n, j);
graph::addEdge(j + n, i);
} else if (a && !b) {
graph::addEdge(i + n, j + n);
graph::addEdge(j, i);
} else if (!a && b) {
graph::addEdge(i, j);
graph::addEdge(j + n, i + n);
} else {
graph::addEdge(i, j + n);
graph::addEdge(j, i + n);
}
}
}
int main() {
#ifdef forever23
freopen("test.in", "r", stdin);
//freopen("test.out", "w", stdout);
#endif
init();
graph::kosaraju();
for (int i = 1; i <= n; ++i) {
if (bel[i] == bel[i + n]) {
puts("IMPOSSIBLE");
return 0;
}
}
puts("POSSIBLE");
for (int i = 1; i <= n; ++i) {
printf("%d ", bel[i] > bel[i + n]);
}
return 0;
}
洛谷P4171
題意
每個變數有兩種取值，所以問題就是求解一個\(2-SAT\)
題解
建圖和上一題一模一樣：
\(\begin{cases} A'->B, B'->A & A:h,B:h\\ A'->B', B->A & A:h,B:m \\ A->B, B'->A' & A:m,B:h \\ A->B', B->A' & A:m,B:m \end{cases}\)
只要看有沒有\(x\)和\(x'\)在同一個強聯通分量即可。
程式碼
// Author: 23forever
#include <bits/stdc++.h>
typedef long long LL;
const int MAXN = 200;
using namespace std;
inline int read() {
int x = 0, w = 1;
char c = ' ';
while (!isdigit(c)) {
c = getchar();
if (c == '-') w = -1;
}
while (isdigit(c)) {
x = (x << 1) + (x << 3) + (c ^ 48);
c = getchar();
}
return x * w;
}
int n, m, bel[MAXN + 5], scc_num;
namespace graph {
const int MAXM = 2000;
struct Edge {
int to, nxt;
Edge() {}
Edge(int _to, int _nxt) : to(_to), nxt(_nxt) {}
} edge[MAXM + 5];
int tot, head[MAXN + 5];
inline void addEdge(int u, int v) {
edge[tot] = Edge(v, head[u]), head[u] = tot++;
}
inline void init() {
tot = 0, memset(head, -1, sizeof(head));
}
int dfn[MAXN + 5], low[MAXN + 5], idx;
bool in_sta[MAXN + 5];
stack < int > sta;
void dfs(int u) {
dfn[u] = low[u] = ++idx;
sta.push(u);
in_sta[u] = true;
for (int i = head[u]; ~i; i = edge[i].nxt) {
int v = edge[i].to;
if (!dfn[v]) {
dfs(v);
low[u] = min(low[u], low[v]);
} else if (in_sta[v]) {
low[u] = min(low[u], dfn[v]);
}
}
if (dfn[u] == low[u]) {
++scc_num;
int k;
do {
k = sta.top(), bel[k] = scc_num;
in_sta[k] = false, sta.pop();
} while (k != u);
}
}
void tarjan() {
memset(dfn, 0, sizeof(dfn));
for (int i = 1; i <= 2 * n; ++i) {
if (!dfn[i]) dfs(i);
}
}
}
void init() {
graph::init();
n = read(), m = read();
for (int i = 1; i <= m; ++i) {
char c1 = getchar();
while (!isalpha(c1)) c1 = getchar();
int x = read();
char c2 = getchar();
while (!isalpha(c2)) c2 = getchar();
int y = read();
if (c1 == 'h' && c2 == 'h') {
graph::addEdge(y + n, x);
graph::addEdge(x + n, y);
} else if (c1 == 'h' && c2 == 'm') {
graph::addEdge(x + n, y + n);
graph::addEdge(y, x);
} else if (c1 == 'm' && c2 == 'h') {
graph::addEdge(x, y);
graph::addEdge(y + n, x + n);
} else {
graph::addEdge(x, y + n);
graph::addEdge(y, x + n);
}
}
}
int main() {
#ifdef forever23
freopen("test.in", "r", stdin);
//freopen("test.out", "w", stdout);
#endif
int t = read();
while (t--) {
init();
graph::tarjan();
bool f = false;
for (int i = 1; i <= n; ++i) {
if (bel[i] == bel[i + n]) {
puts("BAD");
f = true;
break;
}
}
if (!f) puts("GOOD");
}
return 0;
}
總結
求解\(2-SAT\)問題其實是通過巧妙的建圖方法來解決。這種能推出就拉邊的思想十分常見。在並查集相關題目中也能見到。值得積累。