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$拆成$x$和$x’$。$x$表示变量$x$值为真,$x’$表示变量$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$问题其实是通过巧妙的建图方法来解决。这种能推出就拉边的思想十分常见。在并查集相关题目中也能见到。值得积累。

本博客所有文章均采用 CC BY-NC-SA 4.0 许可协议,转载请注明出处
本文链接:https://23forever.com/2019/07/05/2-sat/