Skip to content

2-SAT

SAT stands for the Satisfiability problem. The general form is the k-Satisfiability problem, abbreviated as k-SAT. When \(k>2\), the problem is NP-complete. Therefore, we only study the case where \(k=2\).

Definition

2-SAT, simply put, involves giving \(n\) Boolean equations, each related to two variables, such as \(a \vee b\), meaning that at least one of the variables \(a\) and \(b\) must be satisfied. The goal is to determine whether a feasible assignment exists. Clearly, there may be multiple possible assignments; typically, the problem only requires finding one. Additionally, \(\neg a\) denotes the negation of \(a\).

Solution Approach

Luogu P4782「Template」2-SAT

There are \(n\) Boolean variables \(x_1\sim x_n\), and \(m\) conditions that must be satisfied. Each condition is of the form "either \(x_i\) is true/false or \(x_j\) is true/false". For example, "\(x_1\) is true or \(x_3\) is false", "\(x_7\) is false or \(x_2\) is false".

The goal of the 2-SAT problem is to assign values to each variable such that all conditions are satisfied.

Represent the above problem using Boolean equations. Let \(a\) denote that \(x_a\) is true (\(\neg a\) then denotes that \(x_a\) is false). If someone's requirement is \(a\) and \(b\), i.e., \((a \vee b)\) (at least one of variables \(a\) and \(b\) must be satisfied). Construct a directed graph for these variable relations: represent \(a\) being true or false as nodes in the graph, and add edges \(\neg a\to b\) and \(\neg b\to a\), meaning that if \(a\) is not satisfied, then \(b\) must be satisfied; similarly, if \(b\) is not satisfied, then \(a\) must be satisfied. After constructing the graph, we can use a strongly connected components (SCC) algorithm to solve the 2-SAT problem.

Original Expression Graph Construction
\(\neg a \vee b\) \(a \to b\) and \(\neg b \to \neg a\)
\(a \vee b\) \(\neg a \to b\) and \(\neg b \to a\)
\(\neg a\vee\neg b\) \(a \to \neg b\) and \(b \to \neg a\)

Many 2-SAT problems require identifying relationships such as: if \(a\) is not satisfied, then \(b\) must be satisfied.

Solving

Consider what it means if two nodes are in the same strongly connected component. Based on the logical meaning of the edges described earlier: if two nodes are in the same SCC, then the conditions they represent must either both be satisfied or both not be satisfied.

After constructing the graph, we use Tarjan's algorithm to find SCCs and check whether, for any Boolean variable \(a\), the node representing \(a\) being true and the node representing \(a\) being false are in the same SCC (a condition cannot be both satisfied and not satisfied, or neither satisfied nor not satisfied). If such a case exists, output "no solution"; otherwise, a solution exists.

When outputting a solution, the value of a variable can be determined by its topological order in the graph. If the topological order of variable \(x\) comes after \(\neg x\), then assign \(x\) as true. Applying this to Tarjan's SCC condensation: assign \(x\) as true when the SCC ID of \(x\) is smaller than that of \(\neg x\). This is because Tarjan's algorithm uses a stack; after running Tarjan and condensing SCCs, a larger topological order corresponds to being visited later in Tarjan, popped earlier from the stack, and thus assigned a smaller SCC ID. Therefore, the SCC IDs obtained by Tarjan correspond to the reverse topological order.

The algorithm traverses the entire graph once. Since \(n\) and \(m\) are of the same order, the complexity for computing the answer is \(O(n)\), so the total complexity is \(O(n)\).

Code Implementation 
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
#include <algorithm>
#include <cstdio>
#include <stack>
using namespace std;
const int N = 2e6 + 2;
int n, m, dfn[N], low[N], t, tot, head[N], a[N];
bool vis[N];
stack<int> s;

struct node {
  int to, Next;
} e[N];

void adde(int u, int v) {
  e[++tot].to = v;
  e[tot].Next = head[u];
  head[u] = tot;
}

void Tarjan(int u) {
  dfn[u] = low[u] = ++t;
  s.push(u);
  vis[u] = 1;
  for (int i = head[u]; i; i = e[i].Next) {
    int v = e[i].to;
    if (!dfn[v]) {
      Tarjan(v);
      low[u] = min(low[u], low[v]);
    } else if (vis[v])
      low[u] = min(low[u], dfn[v]);
  }
  if (dfn[u] == low[u]) {
    int cur;
    ++tot;
    do {
      cur = s.top();
      s.pop();
      vis[cur] = 0;
      a[cur] = tot;
    } while (cur != u);
  }
}

int main() {
  scanf("%d%d", &n, &m);
  for (int i = 1, I, J, A, B; i <= m; i++) {
    scanf("%d%d%d%d", &I, &A, &J, &B);
    adde(A ? I + n : I, B ? J : J + n);
    adde(B ? J + n : J, A ? I : I + n);
  }
  tot = 0;
  for (int i = 1; i <= (n << 1); i++)
    if (!dfn[i]) Tarjan(i);
  for (int i = 1; i <= n; i++) {
    if (a[i] == a[i + n]) {
      printf("IMPOSSIBLE");
      return 0;
    }
  }
  puts("POSSIBLE");
  for (int i = 1; i <= n; i++)
    printf("%c%c", a[i] < a[i + n] ? '1' : '0', " \n"[i == n]);
  return 0;
}

Examples

Example 1

HDU3062 Party

\(n\) couples are invited to a party, but due to space constraints, only one person from each couple can attend. Among the \(2n\) people, some have significant conflicts (of course, there is no conflict between spouses), and two people in conflict will not appear at the party at the same time. Is it possible for \(n\) people to attend simultaneously?

Following the analysis above, if the husband from \(a_1\) and the wife from \(a_2\) are in conflict, we connect the husband from \(a_1\) to the husband from \(a_2\), and the wife from \(a_2\) to the wife from \(a_1\). Then, we perform SCC condensation and coloring to check.

Reference Code 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
```cpp
#include <algorithm>
#include <cstring>
#include <iostream>
constexpr int MAXN = 2018;
constexpr int 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) {  // If you don't understand the contraction point, please refer to the strongly connected components section (there is a link above).
  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;  // Coloring
      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 false;
  return true;
}

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() {
  cin.tie(nullptr)->sync_with_stdio(false);
  while (cin >> n >> m) {
    init();
    for (int i = 1; i <= m; i++) {
      int a1, a2, c1, c2;
      cin >> a1 >> a2 >> c1 >> c2;
      add(2 * a1 + c1, 2 * a2 + 1 - c2);
      // For the i-th couple, we use 2i+1 to represent the husband and 2i to represent the wife.
      add(2 * a2 + c2, 2 * a1 + 1 - c1);
    }
    if (solve())
      cout << "YES\n";
    else
      cout << "NO\n";
  }
  return 0;
}
```

Example 2

2018-2019 ACM-ICPC Asia Seoul Regional K TV Show Game

There are \(k\) lights, each either red or blue, but the initial colors are unknown. There are \(n\) people, each choosing three lights and guessing their colors. A person wins a prize if they guess at least two colors correctly. Determine whether there exists a coloring scheme for the lights such that everyone can win a prize. If so, output one such coloring scheme.

According to Wu Yu - "Solving 2-SAT Problems Using Symmetry", we can conclude: to output a feasible solution for a 2-SAT problem, it suffices to make selections and deletions in a bottom-up manner on the DAG obtained after Tarjan SCC condensation.

In practice, this can be achieved by constructing the reverse graph of the DAG and performing topological sorting on it. Alternatively, based on the property that after Tarjan condensation, nodes with smaller SCC IDs are closer to leaf nodes, we can prioritize selecting nodes with smaller SCC IDs.

Below is the code for the second implementation method.

Reference Code 
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
#include <algorithm>
#include <iostream>
using namespace std;
constexpr int MAXN = 1e4 + 5;
constexpr int MAXK = 5005;

int n, k;
int id[MAXN][5];
char s[MAXN][5][5], ans[MAXK];
bool vis[MAXN];

struct Edge {
  int v, nxt;
} e[MAXN * 100];

int head[MAXN], tot = 1;

void addedge(int u, int v) {
  e[tot].v = v;
  e[tot].nxt = head[u];
  head[u] = tot++;
}

int dfn[MAXN], low[MAXN], color[MAXN], stk[MAXN], ins[MAXN], top, dfs_clock, c;

void tarjan(int x) {  // Tarjan algorithm to find strongly connected components
  stk[++top] = x;
  ins[x] = 1;
  dfn[x] = low[x] = ++dfs_clock;
  for (int i = head[x]; i; i = e[i].nxt) {
    int v = e[i].v;
    if (!dfn[v]) {
      tarjan(v);
      low[x] = min(low[x], low[v]);
    } else if (ins[v])
      low[x] = min(low[x], dfn[v]);
  }
  if (dfn[x] == low[x]) {
    c++;
    do {
      color[stk[top]] = c;
      ins[stk[top]] = 0;
    } while (stk[top--] != x);
  }
}

int main() {
  cin.tie(nullptr)->sync_with_stdio(false);
  cin >> k >> n;
  for (int i = 1; i <= n; i++) {
    for (int j = 1; j <= 3; j++) cin >> id[i][j] >> s[i][j];

    for (int j = 1; j <= 3; j++) {
      for (int k = 1; k <= 3; k++) {
        if (j == k) continue;
        int u = 2 * id[i][j] - (s[i][j][0] == 'B');
        int v = 2 * id[i][k] - (s[i][k][0] == 'R');
        addedge(u, v);
      }
    }
  }

  for (int i = 1; i <= 2 * k; i++)
    if (!dfn[i]) tarjan(i);

  for (int i = 1; i <= 2 * k; i += 2)
    if (color[i] == color[i + 1]) {
      cout << "-1\n";
      return 0;
    }

  for (int i = 1; i <= 2 * k; i += 2) {
    int f1 = color[i], f2 = color[i + 1];
    if (vis[f1]) {
      ans[(i + 1) >> 1] = 'R';
      continue;
    }
    if (vis[f2]) {
      ans[(i + 1) >> 1] = 'B';
      continue;
    }
    if (f1 < f2) {
      vis[f1] = true;
      ans[(i + 1) >> 1] = 'R';
    } else {
      vis[f2] = true;
      ans[(i + 1) >> 1] = 'B';
    }
  }
  ans[k + 1] = 0;
  cout << (ans + 1) << '\n';
  return 0;
}

Exercises

本页面最近更新：，更新历史
发现错误？想一起完善？ 在 GitHub 上编辑此页！
本页面贡献者：OI-wiki
本页面的全部内容在 CC BY-SA 4.0 和 SATA 协议之条款下提供，附加条款亦可能应用