PrevNext
Rare
 0/18

Strongly Connected Components

Authors: Benjamin Qi, Dong Liu, Neo Wang, Rameez Parwez

Subsets of nodes in directed graphs where each node in a subset can reach each other node in the subset.

SCCs

Focus Problem – try your best to solve this problem before continuing!

View Internal Solution

The definition of a kingdom in this problem is equivalent to the definition of a strongly connected component. We can compute these components using either Kosaraju's or Tarjan's algorithms, both of which are described below.

Kosaraju's Algorithm

Solution (Kosaraju's)

C++

#include <bits/stdc++.h>
using namespace std;
using vi = vector<int>;
#define pb push_back
const int mx = 1e5 + 1;
// adj_t is the transpose of adj
vi adj[mx], adj_t[mx], S;

Java

import java.io.*;
import java.util.*;
public class Main {
static final int N = 100001;
static boolean[] vis = new boolean[N + 1];
// Adjacency list of neighbor
static List<Integer>[] adj = new ArrayList[N + 1];
// adjT is the transpose of adj
static List<Integer>[] adjT = new ArrayList[N + 1];

Tarjan's Algorithm

Solution (Tarjan's)

C++

#include <bits/stdc++.h>
using namespace std;
/**
* Description: Tarjan's, DFS once to generate
* strongly connected components in topological order. $a,b$
* in same component if both $a\to b$ and $b\to a$ exist.
* Uses less memory than Kosaraju b/c doesn't store reverse edges.
* Time: O(N+M)
* Source: KACTL
* https://github.com/kth-competitive-programming/kactl/blob/master/content/graph/SCC.h

Problems

StatusSourceProblem NameDifficultyTags
CSESEasy
Show TagsDP, SCC
POIEasy
Show TagsDP, SCC
CFNormal
Show TagsDP, SCC
Old GoldNormal
Show TagsSCC
CFNormal
Show TagsSCC
CFHard
Show TagsSCC
POIHard
Show TagsSCC
KattisHard
Show TagsSCC
CSESVery Hard
Show TagsSCC

2-SAT

Resources

Resources
CF
cp-algo
Algorithms Live!

Introduction

The 2-Satisfiability (2-SAT) problem is a specific type of Boolean satisfiability problem where each clause in the given formula contains exactly two literals. The task is to determine whether there exists an assignment of truth values to the variables such that the entire formula is satisfied. A literal is either a variable or its negation. The formula is represented in Conjunctive Normal Form (CNF), which means it is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of exactly two literals.

Algorithm

To solve a 2-SAT problem, consider a Boolean formula in Conjunctive Normal Form (CNF) where each clause contains exactly two literals, such as

(¬x1x2)(x1¬x2)(¬x2x3)(\lnot x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_2 \lor x_3)

The algorithm proceeds by constructing an implication graph, a directed graph where each variable xix_i and its negation ¬xi\lnot x_i are represented as nodes. For each clause (ab)(a \lor b), we add two directed edges: ¬ab\lnot a \rightarrow b and ¬ba\lnot b \rightarrow a. These edges reflect the logical implications necessary to satisfy each clause.

Once the implication graph is constructed, the next step is to identify the strongly connected components (SCCs) of the graph. This can be achieved using Kosaraju's or Tarjan's algorithm, both of which run in linear time. An SCC is a maximal subgraph where every node is reachable from every other node within the subgraph, indicating a tight group of variables and implications.

After identifying the SCCs, we check for consistency. Specifically, we need to ensure that no variable xix_i and its negation ¬xi\lnot x_i belong to the same SCC. If such a scenario occurs, it indicates a logical contradiction because it implies that xix_i must be both true and false simultaneously, rendering the formula unsatisfiable.

If the graph passes the consistency check, we proceed to determine a satisfying assignment for the variables. This is done by processing the SCCs in topologically sorted order. Topological sorting of the SCCs respects the direction of the implications, ensuring that dependencies are correctly managed. Starting from any SCC with no incoming edges, we assign a truth value to one variable in each SCC. Typically, we set variables to true initially and then propagate this assignment through the graph, ensuring that all implications are satisfied. If a variable is already assigned a truth value due to previous propagations, we skip it to avoid conflicts.

For example, in the formula (¬x1x2)(x1¬x2)(¬x2x3)(\lnot x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_2 \lor x_3), the implication graph would have edges (¬x1x2),(¬x2x1),(x1¬x2),(x2¬x1),(¬x2x3)(\lnot x_1 \rightarrow x_2), (\lnot x_2 \rightarrow x_1), (x_1 \rightarrow \lnot x_2), (x_2 \rightarrow \lnot x_1), (\lnot x_2 \rightarrow x_3) and (¬x3x2)\lnot x_3 \rightarrow x_2). After constructing the graph and finding the SCCs, we check for consistency. Assuming no contradictions are found, we then assign truth values based on the topological order of the SCCs.

This approach ensures that the 2-SAT problem can be solved efficiently, in linear time relative to the number of variables and clauses, leveraging the properties of directed graphs and the power of SCCs to manage logical dependencies and implications systematically. This makes the 2-SAT problem a notable example of a problem that is solvable in polynomial time, despite being a specific case of the generally intractable Boolean satisfiability problem.

Implementation

Now, let's implement the entire algorithm for solving the 2-SAT problem using Kosaraju's algorithm. First, we construct the graph of implications (adj)('adj') and find all strongly connected components (SCCs). Kosaraju's algorithm efficiently identifies SCCs in O(n+m)O(n + m) time complexity. During the second traversal of the graph, Kosaraju's algorithm visits these SCCs in topological order, allowing us to assign a component number comp[v]comp[v]to each vertex vv.

Subsequently, to determine the satisfiability of the 2-SAT problem:

  • For each variable xx, we compare comp[x]comp[x] and comp[¬x]comp[\lnot x]. If comp[x]=comp[¬x]comp[x] = comp[\lnot x], it indicates that both xx and ¬x\lnot x belong to same SCCs, implying a contradiction.
  • In such cases, we return falsefalse to indicate that no valid assignment satisfies the 2-SAT problem.

Below is the implementation of the solution for the 2-SAT problem, utilizing the graph of implications adjadj and its transpose adjTadj^T, where vertices 2k2k and 2k+12k+1 correspond to variable kk and its negation respectively.

C++

struct TwoSatSolver {
int n_vars;
int n_vertices;
vector<vector<int>> adj, adj_t;
vector<bool> used;
vector<int> order, comp;
vector<bool> assignment;
TwoSatSolver(int _n_vars)
: n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices),

Focus Problem – try your best to solve this problem before continuing!

It is a straightforward 2SAT problem. Each topping corresponds to a variable. When a topping xx is preferred with '+', we include xx in our clause. For preference '-', we include ¬x\lnot x in the clause.

Solution

C++

#include <bits/stdc++.h>
using namespace std;
struct TwoSatSolver {
int n_vars;
int n_vertices;
vector<vector<int>> adj, adj_t;
vector<bool> used;
vector<int> order, comp;
vector<bool> assignment;

Problems

StatusSourceProblem NameDifficultyTags
CFEasy
Show Tags2SAT
CFEasy
Show Tags2SAT, DFS, DSU
CCEasy
Show Tags2SAT, DSU, Greedy, Sliding Window
KattisEasy
Show Tags2SAT
ACNormal
Show Tags2SAT
CFHard
Show Tags2SAT, Binary Search, Trees
CFHard
Show Tags2SAT, DFS

Module Progress:

Join the USACO Forum!

Stuck on a problem, or don't understand a module? Join the USACO Forum and get help from other competitive programmers!

PrevNext