2-SAT | pinkyHead's blog

算法简介

给出若干个元素，其中每个元素非真即假。然后再给出若干个包含这些元素的命题，要求找出这些元素的可能取值，使得所有给出的命题成立。

问题的初始模型网上都已经讲的很清楚了，具体可以参考传送门。这里我只会放一些本人在的学习过程中踩过的坑

Tarjan 缩点

一般来说，2-SAT 的模型所建出来的图都是对称的。这里的对称该如何理解呢？

给出两个元素A，B。那么如果A，B不能共存，那么A->B’,B->A’。即如果选了A，那么只能选B’;如果选了B，那么只能选A’。所以如果能由X推出Y，那么就能从Y’推出X’，这就是所谓的"对称"。

先使用 tarjan 算法跑一边强连通分量，如果存在一个元素X能推出元素X’,那么说明X’也能推出X，所以一定会导致矛盾产生，那么问题一定无解。

如果问题有解，那么我们就反向拓扑排序，依次选择排序过程中遇到的点。由于求强连通分量的时候利用了栈，这就是一个天然的反向拓扑排序的结构，所以选择最先进栈的强连通分量就行了。

至于为什么需要反向拓扑排序，其实博主也不能严格证明出它的正确性，这个需要自己感性理解。首先可以先自己推算一下，可以发现正向排序或者不进行排序随意选都是会导致错误的。然后可以发现反向排序选点时，选点后不会产生矛盾，从而对明白这个方法的正确性。

//模板题：HDU3062 Party
#include <algorithm>
#include <cstdio>
#include <cstring>
#include <iostream>
#define maxn 2018
#define maxm 4000400
using namespace std;
int Index, instack[maxn], DFN[maxn], LOW[maxn];
int tot, color[maxn];
int numedge, head[maxn];
struct Edge {
  int nxt, to;
} edge[maxm];
int sta[maxn], top;
int n, m;
void add(int x, int y) {
  edge[++numedge].to = y;
  edge[numedge].nxt = head[x];
  head[x] = numedge;
}
void tarjan(int x) {  // 缩点看不懂请移步强连通分量上面有一个链接可以点。
  sta[++top] = x;
  instack[x] = 1;
  DFN[x] = LOW[x] = ++Index;
  for (int i = head[x]; i; i = edge[i].nxt) {
    int v = edge[i].to;
    if (!DFN[v]) {
      tarjan(v);
      LOW[x] = min(LOW[x], LOW[v]);
    } else if (instack[v])
      LOW[x] = min(LOW[x], DFN[v]);
  }
  if (DFN[x] == LOW[x]) {
    tot++;
    do {
      color[sta[top]] = tot;  // 染色
      instack[sta[top]] = 0;
    } while (sta[top--] != x);
  }
}
bool solve() {
  for (int i = 0; i < 2 * n; i++)
    if (!DFN[i]) tarjan(i);
  for (int i = 0; i < 2 * n; i += 2)
    if (color[i] == color[i + 1]) return 0;
  return 1;
}
void init() {
  top = 0;
  tot = 0;
  Index = 0;
  numedge = 0;
  memset(sta, 0, sizeof(sta));
  memset(DFN, 0, sizeof(DFN));
  memset(instack, 0, sizeof(instack));
  memset(LOW, 0, sizeof(LOW));
  memset(color, 0, sizeof(color));
  memset(head, 0, sizeof(head));
}
int main() {
  while (~scanf("%d%d", &n, &m)) {
    init();
    for (int i = 1; i <= m; i++) {
      int a1, a2, c1, c2;
      scanf("%d%d%d%d", &a1, &a2, &c1, &c2);  // 自己做的时候别用 cin 会被卡
      add(2 * a1 + c1, 2 * a2 + 1 - c2);
      // 对于第 i 对夫妇，我们用 2i+1 表示丈夫，2i 表示妻子。
      add(2 * a2 + c2, 2 * a1 + 1 - c1);
    }
    if (solve())
      printf("YES\n");
    else
      printf("NO\n");
  }
  return 0;
}

暴搜

沿着图上一条路径，如果一个点被选择了，那么这条路径以后的点都将被选择，那么，出现不可行的情况就是，存在一个集合中两者都被选择了。如果产生不合法的情况，那么我们就对刚才的操作清零，然后再选择当前点的反点，如果问题仍然不合法，那么问题无解。这个方法的正确性是显然的。

同时，由于图的对称性可知，这样做是不需要回溯的（这里如果不懂，仍然可以参考传送门），所以复杂度是严格的 $O(mn)$ 。

但是tarjan缩点的算法复杂度是 $O(m+n)$ ，为什么这里还要引入暴搜呢？其实暴搜的优点在于，它能满足一些特殊限制，比如可以很容易得到字典序最小的解，然而tarjan缩点是做不到的

// 暴搜模板（刘汝佳白书第 323 页）
struct Twosat {
  int n;
  vector<int> g[maxn * 2];
  bool mark[maxn * 2];
  int s[maxn * 2], c;
  bool dfs(int x) {
    if (mark[x ^ 1]) return false;
    if (mark[x]) return true;
    mark[x] = true;
    s[c++] = x;
    for (int i = 0; i < (int)g[x].size(); i++)
      if (!dfs(g[x][i])) return false;
    return true;
  }
  void init(int n) {
    this->n = n;
    for (int i = 0; i < n * 2; i++) g[i].clear();
    memset(mark, 0, sizeof(mark));
  }
  void add_clause(int x, int y) {  // 这个函数随题意变化
    g[x].push_back(y ^ 1);         // 选了 x 就必须选 y^1
    g[y].push_back(x ^ 1);
  }
  bool solve() {
    for (int i = 0; i < n * 2; i += 2)
      if (!mark[i] && !mark[i + 1]) {
        c = 0;
        if (!dfs(i)) {
          while (c > 0) mark[s[--c]] = false;
          if (!dfs(i + 1)) return false;
        }
      }
    return true;
  }
};