AIOJ

SAT is short for the satisfiability problem. Its general form is the k-satisfiability problem, abbreviated k-SAT. When $k>2$ , the problem is NP-complete, so we study only the case $k=2$ .

Definition

In simple terms, 2-SAT gives $n$ Boolean equations, each involving two variables, such as $a \vee b$ , meaning that at least one of the variables $a, b$ is satisfied. We then determine whether a feasible assignment exists. There may be multiple feasible assignments; in most problems, finding any one is enough. In addition, $\neg a$ means that $a$ is negated.

Solution Idea

Luogu P4782 “2-SAT Template”

There are $n$ Boolean variables $x_1\sim x_n$ and $m$ conditions to satisfy. Each condition has the form “ $x_i$ is true/false or $x_j$ is true/false.” For example, “ $x_1$ is true or $x_3$ is false” and “ $x_7$ is false or $x_2$ is false.”

The goal of 2-SAT is to assign a value to each variable so that all conditions are satisfied.

Represent the problem above with Boolean equations. Let $a$ mean that $x_a$ is true ( $\neg a$ means that $x_a$ is false). If someone's requirements are $a$ and $b$ , that is, $(a \vee b)$ (at least one of the variables $a, b$ is satisfied), construct a directed graph for these relationships. Represent whether $a$ is true or false by vertices of the graph; $\neg a\to b$ $\neg b\to a$ means that if $a$ is false, then $b$ is necessarily true. Similarly, if $b$ is false, then $a$ is necessarily true. After constructing the graph, we can solve 2-SAT by contracting strongly connected components.

Original clause	Implication graph
$\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 finding relationships such as: if $a$ is false, then $b$ is true.

Solving

Consider what it means for two vertices to lie in the same strongly connected component. From the logical meaning of the edges above, if two vertices lie in the same SCC, then the conditions they represent are either both satisfied or both unsatisfied.

After constructing the graph, use Tarjan algorithm for finding SCCs to find SCCs. For every Boolean variable $a$ , determine whether the vertex representing $a$ being true and the vertex representing $a$ being false lie in the same SCC (one condition cannot be both satisfied and unsatisfied, or be both unsatisfied and not unsatisfied). If so, output that there is no solution; otherwise, a solution exists.

To output an assignment, determine each variable's value from its topological order in the graph. If the topological order of variable $x$ comes after that of $\neg x$ , set $x$ to true. After applying Tarjan's SCC contraction, this means that when the SCC containing $x$ has a number before that of $\neg x$ , set $x$ to true. Tarjan's algorithm uses a stack when finding SCCs: a component with a larger topological order is visited later by Tarjan, popped from the stack and contracted earlier, and therefore receives a smaller component number. Thus, the SCC numbers produced by Tarjan correspond to the reverse topological order.

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

Implementation

#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

There are $n$ couples invited to a party. Because of venue constraints, only one person from each couple can attend. Among the $2n$ people, some pairs have serious conflicts (of course, spouses do not conflict), and two people with a conflict cannot attend together. Is it possible for $n$ people to attend simultaneously?

Following the analysis above, if the husband from $a_1$ conflicts with the wife from $a_2$ , add an edge from the husband of $a_1$ to the husband of $a_2$ , and from the wife of $a_2$ to the wife of $a_1$ ; then contract the SCCs and assign components to determine the answer.

Reference Code

#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 SCC contraction is unclear, see the linked strongly connected components page 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;  // Assign the component
      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, 2i+1 denotes the husband and 2i denotes 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$ lamps, each red or blue, but their initial colors are unknown. There are $n$ people; each chooses three lamps and guesses their colors. A person wins a prize if at least two guesses are correct. Determine whether there is a coloring in which everyone wins, and if so, output one such coloring.

According to Yu Wu — Solving 2-SAT Problems by Symmetry, to output a feasible solution to a 2-SAT problem, choose and delete vertices from the bottom up in the DAG obtained after SCC contraction.

In practice, this can be implemented by constructing the reverse graph of the DAG and performing a topological sort on it. Alternatively, after Tarjan's contraction, use the fact that a smaller component number means a vertex is closer to a leaf, and prioritize vertices with smaller component numbers.

The second implementation is given below.