Strongly Connected Components

SCCs

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)

Copy
#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;

Copy
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)

Copy
#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

2-SAT

Resources

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

The algorithm proceeds by constructing an implication graph, a directed graph where each variable $x_i$ and its negation $\lnot x_i$ are represented as nodes. For each clause $(a \lor b)$, we add two directed edges: $\lnot a \rightarrow b$ and $\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 $x_i$ and its negation $\lnot x_i$ belong to the same SCC. If such a scenario occurs, it indicates a logical contradiction because it implies that $x_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 $(\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 $(\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 ($\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')$ and find all strongly connected components (SCCs). Kosaraju's algorithm efficiently identifies SCCs in $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]$to each vertex $v$.

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

• For each variable $x$, we compare $comp[x]$ and $comp[\lnot x]$. If $comp[x] = comp[\lnot x]$, it indicates that both $x$ and $\lnot x$ belong to same SCCs, implying a contradiction.
• In such cases, we return $false$ 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 $adj$ and its transpose $adj^T$, where vertices $2k$ and $2k+1$ correspond to variable $k$ and its negation respectively.

Copy
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),

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

Solution

Copy
#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