From 611de4aaa28d72b37cada5a94b2402a947774c83 Mon Sep 17 00:00:00 2001 From: Rameez Parwez Date: Sat, 22 Jun 2024 23:46:33 +0530 Subject: [PATCH 01/32] update SSC.mdx and SSC.problems.mdx --- content/6_Advanced/SCC.mdx | 233 +++++++++++++++++++++++++-- content/6_Advanced/SCC.problems.json | 86 ++++++++++ 2 files changed, 308 insertions(+), 11 deletions(-) diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index 2bb574e36f..bd470c2da1 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -1,7 +1,7 @@ --- id: SCC title: 'Strongly Connected Components' -author: Benjamin Qi, Dong Liu, Neo Wang +author: Benjamin Qi, Dong Liu, Neo Wang, Rameez Parwez prerequisites: - toposort - BCC-2CC @@ -258,15 +258,7 @@ int main() { ## 2-SAT - - - - -implementation - - - -### Tutorial +### Resources @@ -274,8 +266,227 @@ implementation +## Introduction +The 2-Satisfiability (2-SAT) problem is a specific type of [Boolean satisfiability problem](https://en.wikipedia.org/wiki/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)](https://en.wikipedia.org/wiki/Conjunctive_normal_form), 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 + +$$ +(\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 $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)](https://en.wikipedia.org/wiki/Strongly_connected_component) 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](https://en.wikipedia.org/wiki/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. + + + +```cpp +struct TwoSatSolver { + int n_vars; + int n_vertices; + vector> adj, adj_t; + vector used; + vector order, comp; + vector assignment; + + TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { + order.reserve(n_vertices); + } + void dfs1(int v) { + used[v] = true; + for (int u : adj[v]) { + if (!used[u]) + dfs1(u); + } + order.push_back(v); + } + + void dfs2(int v, int cl) { + comp[v] = cl; + for (int u : adj_t[v]) { + if (comp[u] == -1) + dfs2(u, cl); + } + } + + bool solve_2SAT() { + order.clear(); + used.assign(n_vertices, false); + for (int i = 0; i < n_vertices; ++i) { + if (!used[i]) + dfs1(i); + } + + comp.assign(n_vertices, -1); + for (int i = 0, j = 0; i < n_vertices; ++i) { + int v = order[n_vertices - i - 1]; + if (comp[v] == -1) + dfs2(v, j++); + } + + assignment.assign(n_vars, false); + for (int i = 0; i < n_vertices; i += 2) { + if (comp[i] == comp[i + 1]) + return false; + assignment[i / 2] = comp[i] > comp[i + 1]; + } + return true; + } + + void add_disjunction(int a, bool na, int b, bool nb) { + // na and nb signify whether a and b are to be negated + a = 2 * a ^ na; + b = 2 * b ^ nb; + int neg_a = a ^ 1; + int neg_b = b ^ 1; + adj[neg_a].push_back(b); + adj[neg_b].push_back(a); + adj_t[b].push_back(neg_a); + adj_t[a].push_back(neg_b); + } + + static void example_usage() { + TwoSatSolver solver(3); // a, b, c + solver.add_disjunction(0, false, 1, true); // a v not b + solver.add_disjunction(0, true, 1, true); // not a v not b + solver.add_disjunction(1, false, 2, false); // b v c + solver.add_disjunction(0, false, 0, false); // a v a + assert(solver.solve_2SAT() == true); + auto expected = vector(True, False, True); + assert(solver.assignment == expected); + } +}; +``` + + + + +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 + + +```cpp +#include +using namespace std; + +struct TwoSatSolver { + int n_vars; + int n_vertices; + vector> adj, adj_t; + vector used; + vector order, comp; + vector assignment; + + TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { + order.reserve(n_vertices); + } + void dfs1(int v) { + used[v] = true; + for (int u : adj[v]) { + if (!used[u]) + dfs1(u); + } + order.push_back(v); + } + + void dfs2(int v, int cl) { + comp[v] = cl; + for (int u : adj_t[v]) { + if (comp[u] == -1) + dfs2(u, cl); + } + } + + bool solve_2SAT() { + order.clear(); + used.assign(n_vertices, false); + for (int i = 0; i < n_vertices; ++i) { + if (!used[i]) + dfs1(i); + } + + comp.assign(n_vertices, -1); + for (int i = 0, j = 0; i < n_vertices; ++i) { + int v = order[n_vertices - i - 1]; + if (comp[v] == -1) + dfs2(v, j++); + } + + assignment.assign(n_vars, false); + for (int i = 0; i < n_vertices; i += 2) { + if (comp[i] == comp[i + 1]) + return false; + assignment[i / 2] = comp[i] > comp[i + 1]; + } + return true; + } + + void add_disjunction(int a, int na, int b, int nb) { + // na and nb signify whether a and b are to be negated + a = 2 * a ^ na; + b = 2 * b ^ nb; + int neg_a = a ^ 1; + int neg_b = b ^ 1; + adj[neg_a].push_back(b); + adj[neg_b].push_back(a); + adj_t[b].push_back(neg_a); + adj_t[a].push_back(neg_b); + } +}; + +int main() { + int n, m; + cin >> n >> m; + TwoSatSolver solver(m); + + for (int i = 1; i <= n; i++) { + int tops1, tops2; + char pref1, pref2; + cin >> pref1 >> tops1 >> pref2 >> tops2; + tops1--, tops2--; + solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); + } + + if (!solver.solve_2SAT()) { + cout << "IMPOSSIBLE" << '\n'; + } else { + for (int i = 0; i < m; i++) { + cout << (!solver.assignment[i] ? '+' : '-') << " \n"[i == m - 1]; + } + } +} +``` + + + +## Problems + + + diff --git a/content/6_Advanced/SCC.problems.json b/content/6_Advanced/SCC.problems.json index 42a19ea33c..cc6028afa8 100644 --- a/content/6_Advanced/SCC.problems.json +++ b/content/6_Advanced/SCC.problems.json @@ -142,5 +142,91 @@ "kind": "none" } } + ], + "2SAT":[ + { + "uniqueId": "cf-1475F", + "name": "Unusual Matrix", + "url": "https://codeforces.com/contest/1475/problem/F", + "source": "CF", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-776D", + "name": "The Door Problem", + "url": "https://codeforces.com/contest/776/problem/D", + "source": "CF", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT", "DSU", "DFS"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cc-HKRMAN", + "name": "Hackerman", + "url": "https://www.codechef.com/LTIME95A/problems/HKRMAN", + "source": "CC", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT", "DSU", "Sliding Window", "Greedy"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "kattis-illumination", + "name": "Illumination", + "url": "https://open.kattis.com/problems/illumination", + "source": "Kattis", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "ac-CoprimeSolitaire", + "name": "Coprime Solitaire", + "url": "https://atcoder.jp/contests/abc210/tasks/abc210_f", + "source": "AC", + "difficulty": "Normal", + "isStarred": true, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-1903F", + "name": "Babysitting", + "url": "https://codeforces.com/problemset/problem/1903/F", + "source": "CF", + "difficulty": "Hard", + "isStarred": true, + "tags": ["2SAT", "Binary Search", "Trees"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-1089H", + "name": "Harder Satisfiability", + "url": "https://codeforces.com/problemset/problem/1089/H", + "source" : "CF", + "difficulty": "Hard", + "isStarred": true, + "tags": ["2SAT", "DFS"], + "solutionMetadata": { + "kind": "internal" + } + } ] } From 4f72da68f9346f68906cf53fc03b8743f54bea80 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sat, 22 Jun 2024 18:20:12 +0000 Subject: [PATCH 02/32] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- content/6_Advanced/SCC.mdx | 310 +++++++++++++-------------- content/6_Advanced/SCC.problems.json | 6 +- 2 files changed, 156 insertions(+), 160 deletions(-) diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index bd470c2da1..4feac6c9b2 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -272,7 +272,7 @@ The 2-Satisfiability (2-SAT) problem is a specific type of [Boolean satisfiabili ## 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 -$$ +$$ (\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 $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. @@ -283,7 +283,7 @@ After identifying the SCCs, we check for consistency. Specifically, we need to e 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](https://en.wikipedia.org/wiki/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 +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. @@ -303,79 +303,77 @@ Below is the implementation of the solution for the 2-SAT problem, utilizing the ```cpp struct TwoSatSolver { - int n_vars; - int n_vertices; - vector> adj, adj_t; - vector used; - vector order, comp; - vector assignment; - - TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { - order.reserve(n_vertices); - } - void dfs1(int v) { - used[v] = true; - for (int u : adj[v]) { - if (!used[u]) - dfs1(u); - } - order.push_back(v); - } - - void dfs2(int v, int cl) { - comp[v] = cl; - for (int u : adj_t[v]) { - if (comp[u] == -1) - dfs2(u, cl); - } - } - - bool solve_2SAT() { - order.clear(); - used.assign(n_vertices, false); - for (int i = 0; i < n_vertices; ++i) { - if (!used[i]) - dfs1(i); - } - - comp.assign(n_vertices, -1); - for (int i = 0, j = 0; i < n_vertices; ++i) { - int v = order[n_vertices - i - 1]; - if (comp[v] == -1) - dfs2(v, j++); - } - - assignment.assign(n_vars, false); - for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) - return false; - assignment[i / 2] = comp[i] > comp[i + 1]; - } - return true; - } - - void add_disjunction(int a, bool na, int b, bool nb) { - // na and nb signify whether a and b are to be negated - a = 2 * a ^ na; - b = 2 * b ^ nb; - int neg_a = a ^ 1; - int neg_b = b ^ 1; - adj[neg_a].push_back(b); - adj[neg_b].push_back(a); - adj_t[b].push_back(neg_a); - adj_t[a].push_back(neg_b); - } - - static void example_usage() { - TwoSatSolver solver(3); // a, b, c - solver.add_disjunction(0, false, 1, true); // a v not b - solver.add_disjunction(0, true, 1, true); // not a v not b - solver.add_disjunction(1, false, 2, false); // b v c - solver.add_disjunction(0, false, 0, false); // a v a - assert(solver.solve_2SAT() == true); - auto expected = vector(True, False, True); - assert(solver.assignment == expected); - } + int n_vars; + int n_vertices; + vector> adj, adj_t; + vector used; + vector order, comp; + vector assignment; + + TwoSatSolver(int _n_vars) + : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), + adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), + assignment(n_vars) { + order.reserve(n_vertices); + } + void dfs1(int v) { + used[v] = true; + for (int u : adj[v]) { + if (!used[u]) dfs1(u); + } + order.push_back(v); + } + + void dfs2(int v, int cl) { + comp[v] = cl; + for (int u : adj_t[v]) { + if (comp[u] == -1) dfs2(u, cl); + } + } + + bool solve_2SAT() { + order.clear(); + used.assign(n_vertices, false); + for (int i = 0; i < n_vertices; ++i) { + if (!used[i]) dfs1(i); + } + + comp.assign(n_vertices, -1); + for (int i = 0, j = 0; i < n_vertices; ++i) { + int v = order[n_vertices - i - 1]; + if (comp[v] == -1) dfs2(v, j++); + } + + assignment.assign(n_vars, false); + for (int i = 0; i < n_vertices; i += 2) { + if (comp[i] == comp[i + 1]) return false; + assignment[i / 2] = comp[i] > comp[i + 1]; + } + return true; + } + + void add_disjunction(int a, bool na, int b, bool nb) { + // na and nb signify whether a and b are to be negated + a = 2 * a ^ na; + b = 2 * b ^ nb; + int neg_a = a ^ 1; + int neg_b = b ^ 1; + adj[neg_a].push_back(b); + adj[neg_b].push_back(a); + adj_t[b].push_back(neg_a); + adj_t[a].push_back(neg_b); + } + + static void example_usage() { + TwoSatSolver solver(3); // a, b, c + solver.add_disjunction(0, false, 1, true); // a v not b + solver.add_disjunction(0, true, 1, true); // not a v not b + solver.add_disjunction(1, false, 2, false); // b v c + solver.add_disjunction(0, false, 0, false); // a v a + assert(solver.solve_2SAT() == true); + auto expected = vector(True, False, True); + assert(solver.assignment == expected); + } }; ``` @@ -392,90 +390,88 @@ It is a straightforward 2SAT problem. Each topping corresponds to a variable. Wh using namespace std; struct TwoSatSolver { - int n_vars; - int n_vertices; - vector> adj, adj_t; - vector used; - vector order, comp; - vector assignment; - - TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { - order.reserve(n_vertices); - } - void dfs1(int v) { - used[v] = true; - for (int u : adj[v]) { - if (!used[u]) - dfs1(u); - } - order.push_back(v); - } - - void dfs2(int v, int cl) { - comp[v] = cl; - for (int u : adj_t[v]) { - if (comp[u] == -1) - dfs2(u, cl); - } - } - - bool solve_2SAT() { - order.clear(); - used.assign(n_vertices, false); - for (int i = 0; i < n_vertices; ++i) { - if (!used[i]) - dfs1(i); - } - - comp.assign(n_vertices, -1); - for (int i = 0, j = 0; i < n_vertices; ++i) { - int v = order[n_vertices - i - 1]; - if (comp[v] == -1) - dfs2(v, j++); - } - - assignment.assign(n_vars, false); - for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) - return false; - assignment[i / 2] = comp[i] > comp[i + 1]; - } - return true; - } - - void add_disjunction(int a, int na, int b, int nb) { - // na and nb signify whether a and b are to be negated - a = 2 * a ^ na; - b = 2 * b ^ nb; - int neg_a = a ^ 1; - int neg_b = b ^ 1; - adj[neg_a].push_back(b); - adj[neg_b].push_back(a); - adj_t[b].push_back(neg_a); - adj_t[a].push_back(neg_b); - } + int n_vars; + int n_vertices; + vector> adj, adj_t; + vector used; + vector order, comp; + vector assignment; + + TwoSatSolver(int _n_vars) + : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), + adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), + assignment(n_vars) { + order.reserve(n_vertices); + } + void dfs1(int v) { + used[v] = true; + for (int u : adj[v]) { + if (!used[u]) dfs1(u); + } + order.push_back(v); + } + + void dfs2(int v, int cl) { + comp[v] = cl; + for (int u : adj_t[v]) { + if (comp[u] == -1) dfs2(u, cl); + } + } + + bool solve_2SAT() { + order.clear(); + used.assign(n_vertices, false); + for (int i = 0; i < n_vertices; ++i) { + if (!used[i]) dfs1(i); + } + + comp.assign(n_vertices, -1); + for (int i = 0, j = 0; i < n_vertices; ++i) { + int v = order[n_vertices - i - 1]; + if (comp[v] == -1) dfs2(v, j++); + } + + assignment.assign(n_vars, false); + for (int i = 0; i < n_vertices; i += 2) { + if (comp[i] == comp[i + 1]) return false; + assignment[i / 2] = comp[i] > comp[i + 1]; + } + return true; + } + + void add_disjunction(int a, int na, int b, int nb) { + // na and nb signify whether a and b are to be negated + a = 2 * a ^ na; + b = 2 * b ^ nb; + int neg_a = a ^ 1; + int neg_b = b ^ 1; + adj[neg_a].push_back(b); + adj[neg_b].push_back(a); + adj_t[b].push_back(neg_a); + adj_t[a].push_back(neg_b); + } }; int main() { - int n, m; - cin >> n >> m; - TwoSatSolver solver(m); - - for (int i = 1; i <= n; i++) { - int tops1, tops2; - char pref1, pref2; - cin >> pref1 >> tops1 >> pref2 >> tops2; - tops1--, tops2--; - solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); - } - - if (!solver.solve_2SAT()) { - cout << "IMPOSSIBLE" << '\n'; - } else { - for (int i = 0; i < m; i++) { - cout << (!solver.assignment[i] ? '+' : '-') << " \n"[i == m - 1]; - } - } + int n, m; + cin >> n >> m; + TwoSatSolver solver(m); + + for (int i = 1; i <= n; i++) { + int tops1, tops2; + char pref1, pref2; + cin >> pref1 >> tops1 >> pref2 >> tops2; + tops1--, tops2--; + solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); + } + + if (!solver.solve_2SAT()) { + cout << "IMPOSSIBLE" << '\n'; + } else { + for (int i = 0; i < m; i++) { + cout << (!solver.assignment[i] ? '+' : '-') << " \n"[i == m - 1]; + } + } } ``` @@ -484,7 +480,7 @@ int main() { ## Problems - diff --git a/content/6_Advanced/SCC.problems.json b/content/6_Advanced/SCC.problems.json index 42a19ea33c..cc6028afa8 100644 --- a/content/6_Advanced/SCC.problems.json +++ b/content/6_Advanced/SCC.problems.json @@ -142,5 +142,91 @@ "kind": "none" } } + ], + "2SAT":[ + { + "uniqueId": "cf-1475F", + "name": "Unusual Matrix", + "url": "https://codeforces.com/contest/1475/problem/F", + "source": "CF", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-776D", + "name": "The Door Problem", + "url": "https://codeforces.com/contest/776/problem/D", + "source": "CF", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT", "DSU", "DFS"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cc-HKRMAN", + "name": "Hackerman", + "url": "https://www.codechef.com/LTIME95A/problems/HKRMAN", + "source": "CC", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT", "DSU", "Sliding Window", "Greedy"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "kattis-illumination", + "name": "Illumination", + "url": "https://open.kattis.com/problems/illumination", + "source": "Kattis", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "ac-CoprimeSolitaire", + "name": "Coprime Solitaire", + "url": "https://atcoder.jp/contests/abc210/tasks/abc210_f", + "source": "AC", + "difficulty": "Normal", + "isStarred": true, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-1903F", + "name": "Babysitting", + "url": "https://codeforces.com/problemset/problem/1903/F", + "source": "CF", + "difficulty": "Hard", + "isStarred": true, + "tags": ["2SAT", "Binary Search", "Trees"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-1089H", + "name": "Harder Satisfiability", + "url": "https://codeforces.com/problemset/problem/1089/H", + "source" : "CF", + "difficulty": "Hard", + "isStarred": true, + "tags": ["2SAT", "DFS"], + "solutionMetadata": { + "kind": "internal" + } + } ] } From 909e43d8e18e54f98a768eac76a659b50d2236af Mon Sep 17 00:00:00 2001 From: Rameez Parwez Date: Sun, 23 Jun 2024 15:46:53 +0530 Subject: [PATCH 12/32] requested changes done --- content/6_Advanced/SCC.mdx | 98 ++++++++++++++++++++++++----------- content/6_Advanced/graph.png | Bin 0 -> 28069 bytes 2 files changed, 68 insertions(+), 30 deletions(-) create mode 100644 content/6_Advanced/graph.png diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index bd470c2da1..4302674ebc 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -273,7 +273,7 @@ The 2-Satisfiability (2-SAT) problem is a specific type of [Boolean satisfiabili To solve a 2-SAT problem, consider a Boolean formula in Conjunctive Normal Form (CNF) where each clause contains exactly two literals, such as $$ -(\lnot x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_2 \lor x_3) +(\lnot x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2) \land (x_1 \lor \lnot x_3) $$ 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. @@ -285,8 +285,11 @@ If the graph passes the consistency check, we proceed to determine a satisfying 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. +(\lnot x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2) \land (x_1 \lor \lnot x_3) +$, the implication graph would have edges $(\lnot x_1 \rightarrow \lnot x_2), (x_1 \rightarrow x_2), (x_1 \rightarrow \lnot x_2), (\lnot x_1 \rightarrow \lnot x_3), (x_2 \rightarrow x_1), (\lnot x_2 \rightarrow \lnot x_1), (x_2 \rightarrow \lnot x_1)$ and $(x_3 \rightarrow x_1)$. +![](graph.png) +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. @@ -313,58 +316,75 @@ struct TwoSatSolver { TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { order.reserve(n_vertices); } + + // Depth-first search for the first pass in Kosaraju's algorithm void dfs1(int v) { used[v] = true; for (int u : adj[v]) { - if (!used[u]) + if (!used[u]) { dfs1(u); + } } - order.push_back(v); + order.push_back(v); // Append node to order list after visiting all reachable nodes } + // Depth-first search for the second pass in Kosaraju's algorithm void dfs2(int v, int cl) { comp[v] = cl; for (int u : adj_t[v]) { - if (comp[u] == -1) + if (comp[u] == -1) { dfs2(u, cl); + } } } - bool solve_2SAT() { + bool solve() { order.clear(); used.assign(n_vertices, false); for (int i = 0; i < n_vertices; ++i) { - if (!used[i]) - dfs1(i); + if (!used[i]) { + dfs1(i); + } } comp.assign(n_vertices, -1); for (int i = 0, j = 0; i < n_vertices; ++i) { int v = order[n_vertices - i - 1]; - if (comp[v] == -1) + if (comp[v] == -1) { dfs2(v, j++); + } } assignment.assign(n_vars, false); for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) - return false; - assignment[i / 2] = comp[i] > comp[i + 1]; + if (comp[i] == comp[i + 1]) { + return false; // If variable and its negation are in the same component, unsatisfiable + } + assignment[i / 2] = comp[i] > comp[i + 1]; // Assign true/false based on component ids } - return true; + return true; // Satisfiable } - void add_disjunction(int a, bool na, int b, bool nb) { - // na and nb signify whether a and b are to be negated + void add_disjunction(int a, int na, int b, int nb) { + // na and nb signify whether a and b are to be negated + + // Convert variable index and negation to node index a = 2 * a ^ na; b = 2 * b ^ nb; + + // Get the negation node index int neg_a = a ^ 1; int neg_b = b ^ 1; + + // Add implication from negation adj[neg_a].push_back(b); adj[neg_b].push_back(a); + + // Add reverse implication for the transposed graph adj_t[b].push_back(neg_a); adj_t[a].push_back(neg_b); } +}; static void example_usage() { TwoSatSolver solver(3); // a, b, c @@ -372,7 +392,7 @@ struct TwoSatSolver { solver.add_disjunction(0, true, 1, true); // not a v not b solver.add_disjunction(1, false, 2, false); // b v c solver.add_disjunction(0, false, 0, false); // a v a - assert(solver.solve_2SAT() == true); + assert(solver.solve() == true); auto expected = vector(True, False, True); assert(solver.assignment == expected); } @@ -391,6 +411,7 @@ It is a straightforward 2SAT problem. Each topping corresponds to a variable. Wh #include using namespace std; +// BeginCodeSnip{2SAT} struct TwoSatSolver { int n_vars; int n_vertices; @@ -402,59 +423,76 @@ struct TwoSatSolver { TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { order.reserve(n_vertices); } + + // Depth-first search for the first pass in Kosaraju's algorithm void dfs1(int v) { used[v] = true; for (int u : adj[v]) { - if (!used[u]) + if (!used[u]) { dfs1(u); + } } - order.push_back(v); + order.push_back(v); // Append node to order list after visiting all reachable nodes } + // Depth-first search for the second pass in Kosaraju's algorithm void dfs2(int v, int cl) { comp[v] = cl; for (int u : adj_t[v]) { - if (comp[u] == -1) + if (comp[u] == -1) { dfs2(u, cl); + } } } - bool solve_2SAT() { + bool solve() { order.clear(); used.assign(n_vertices, false); for (int i = 0; i < n_vertices; ++i) { - if (!used[i]) - dfs1(i); + if (!used[i]) { + dfs1(i); + } } comp.assign(n_vertices, -1); for (int i = 0, j = 0; i < n_vertices; ++i) { int v = order[n_vertices - i - 1]; - if (comp[v] == -1) + if (comp[v] == -1) { dfs2(v, j++); + } } assignment.assign(n_vars, false); for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) - return false; - assignment[i / 2] = comp[i] > comp[i + 1]; + if (comp[i] == comp[i + 1]) { + return false; // If variable and its negation are in the same component, unsatisfiable + } + assignment[i / 2] = comp[i] > comp[i + 1]; // Assign true/false based on component ids } - return true; + return true; // Satisfiable } void add_disjunction(int a, int na, int b, int nb) { - // na and nb signify whether a and b are to be negated + // na and nb signify whether a and b are to be negated + + // Convert variable index and negation to node index a = 2 * a ^ na; b = 2 * b ^ nb; + + // Get the negation node index int neg_a = a ^ 1; int neg_b = b ^ 1; + + // Add implication from negation adj[neg_a].push_back(b); adj[neg_b].push_back(a); + + // Add reverse implication for the transposed graph adj_t[b].push_back(neg_a); adj_t[a].push_back(neg_b); } }; +// EndCodeSnip int main() { int n, m; @@ -469,7 +507,7 @@ int main() { solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); } - if (!solver.solve_2SAT()) { + if (!solver.solve()) { cout << "IMPOSSIBLE" << '\n'; } else { for (int i = 0; i < m; i++) { diff --git a/content/6_Advanced/graph.png b/content/6_Advanced/graph.png new file mode 100644 index 0000000000000000000000000000000000000000..ff03f8cb4d6f4acb261a13016adfcc011b75d9fe GIT binary patch literal 28069 zcmeFac{r5q{{}2sqbNmEXhB63F=ZRo(`uO{*|KE|G0E20hEyt|D6)<=`<8tlQuZ;j zZ!@DX48~~2HfDRT>Gyqp%klp6{{0^P@$|?sGxt5$^;yo(d7jtZ^Xn#;w{P3GjfaP4 z`_(J|+~DEiWpn=%5&*v$bP=xs|J&kw$d|D0qO z{?>!PbK~FH`TskAu=mh?HhmUi&lnp{q4nq#*UWv0 zP9d<@sxW(s?mr>!8?L_O8!0o9IU2?w*X)!x$UMHK8J$PGVZ|-B@7^}S!)U3*1C)oC zY3y}0`t0v-5~*ca{b1Y$TY9I3cL2_Rn229*45Up8LaS?jy!1YupEs%oxRb0y@*A)x zKTNokNan2wc*v9tCf{x~kC^i@c3y8(?Sxp!$iJGaY6Vr;ASe>O22H~0>Z<`!4 zga$#NdTU!YX_a2AdHu=8g%*(=v#K@K8_6C5OWJ)TpUgot{Yo36ib1OaA2h@JZ;w zcX1N(B_X_sT9mi+!jr1_vc@jkr9NE_9SeVOIP+d(lNoArfcUmJWTyAUy^6tGmFs>`-oG1 zgdD{aG0&$SI;GE8?5}697Ngv88sRH7*w7`TILFxq5oQaNc|mPNOgZ`GtczN(l`mMO zhb=Lreq{T>C{Y~Dn-9A7CC+POZvf~A5jQ}{-s}nB6S{fg)sy5ku*SrG6nmweR?Q;A z37^C`0pni7!TZvlq^Z^~f5kWTVv%ebhLnxce;_A@XupsGX&@P6_7p$-{u;F!LE7eQ z$F9g4(VYz6n$ogE=U$#*2#BQd1=Tm6pKLRzZ?X%<2k++X`Jw?*q@0frnZ&n+H(laN zV2nz&U(eau0>qN=3t_leP;X?4vMuS_!oE-rgFspR$*w{&s)*AGFgsdVV0FuZl)#1s zTTJD+_xM>FM*C;|;8jR!S&z1-`5wECuTomrhpif}H!5JE^JW+p1<4^k5>d6R;M`WO z*?ALW)k*l4W+eVs?B(#LtZma*kpf;tdp6~k!v#-cgNDjp%sOBluqzAD)d91p47W{& z+fb(HA#+!?SEIq|(XhHB%Ss#A(vX#pa$ZYe>vhH2-%h|0UE9UvQ7#SSRGx?#kW@)k zUg^?Xcuz#=vW%5<$N+n-6nz(GOL5}FY-+{7vyeX z|0f1k_u4JK9#I%MKKV%>`SL*!*Sa9C5gs~{TX<8Czq*c`eto$p?*h>s`z8jtnT^yQ z+;pkTysS5GiYX3T%{OOY9Qxh#X~|}K8R><)Ef?I8uJBqq2Cfe&s=s&*&1rtnpNcQ1 z&s(6itF+IEgMtI?b?g~` z8qi@GnGSM7v8|#%3*t{i%%)d8x+7~FGPXvdKo_&9I7(Pxg7lN!V1v624VFd85d| zIFQFDh*}sgc|&Ru=Uu0j`I$~X!h!5uccY1ZOmU%=)0BppapXj8+4Q5+f)07_xh?W zAXS<<9k8$mw6!X913d{zPa=Xh`BN^*H?tMg5LYSN&1&PfCl+k~kzssvoJ~h@=r`w` zl|c8{t02D-w~Ok_%a_>EISUzxiD^qawnm($EPs-NsM;@kf)HRjp24z^$Fz~Rl;U~%mp-x(*;o}4j zivYobs(Q-(Q-(gbd-#AY_W2wV%M)>&U)>X?v)nLq0xqpR z5-=f=_6Z&si~_mhn>wpIdsdl^$e?w`1;=V4mk!I(ulRz`_5FTqVn#L4T^|%WV?S#v z%E8D7SiSWL^YNM1L#(wbLKp*&Ep;^*I|Vr)yw0GYIeAL#VkB!J6}_2{w*FGw24(-o z$l#ZsKA)dy0ZVceq_pA8Jy0*cihyoRxa$r6EY6vgw7K^q_(t#(<=gLb*b1R_f@0i4 zTm%vFD`Da(EIV2Piuox=U(5Q$$$RqTNIB-D-E}z?u24ebu0ca{4H}eL3tJ`kB+(}0 z4d_&iMhdsnHw1K6$2?xmzddt2$t&TQj>Z+ngQU9KvZ--^S{5q3- zXYHL+?2i~O;)n*FNXk_Z1d#@xx;gQJEcMl%D7^o$Z7OH8m~*_y!yRW)-!FVEg5U&*_zy95|u%cV>Zj3R?2vI2mZcL zbQ^m{4LK?k{o3cSRd~LABZozS#Dy+81#>c#SWyQ8Ea8c$0O`uaf98{s7TiiJ2Etjk zGxi*)v_hXKA&*8Ju3AI~pf~|DS-7gY29BT3S<ez^ z4NEZ=POTEI$?ZSPOBDm*(u%-~>{RUQ%d#~~i$+nh zL3iQf&D51_XanMRw7srLMaWYw9Fqia%;>HlC@*4{PS&aBl0kK>I-yG`h=$ zcUOu6FFPcgQZR`PZ)v7tT*Ia#B!&W=%2Uw*7N3)o1;UBG?OHpo> z>7o+{RHg#5uUVi(zp>^nL&p}r(pu!$B{i#sa9nWot0iq|p|ldzD`YdjR6*Vd**mZf zAHu3Rw^xNEyF!K|gTJFcrosr$bdjM>^&cudEI)KWb>Mm}2h$VKv=Okl8 zT&Hv08d;*tX_vT(+b5;#DJ+^;aQ4;r);A=fZxCBAb@{-OdghE8JY#bp+hkVWX-Q$~ zB0xoT<|vb@_w~uwxvQuKQqZn1_Ck2m1b=DDd`a#e+5p7t^bTbbIvp`dd#vS4hJA#u zPx`3qO{XvUW$%eHvAv<>Qp*bq`6ZExWX~e)zVv(AE?8rR8`mm`*DPxL{KP7I@akta z{ELHeFJR86O3LXJW)G#iPZK&WjdXoB>*Au>Ttth&dA?0aV4sY(eyY3VFy1XRVn zCdqI}D7O1|sLeNbt)$5k^LXD+e81NUu9fAU>z6tFN>z^>|63{9`quviKfY3XCCfG1 z)oEq$OC1uk6ac=Q2+!_aI*>$qC*A*AbJv)HnGgHBJ@dN}Y&Ffd$6Y<+ux+S-Va6IN zbZzuP_WpGDCyQx35j`S8>~u6AkGQ3Ggy;w34UeSt21+O<6d=`_jF7Bd2ZqqPWr8k~ zx$2=21z$tTQgH?J?`mORJZ4FKtFNMToi_!&Qiva-Rp(#sbQk;8)7+YVBS3LanHevi z_6hloz*>5`ZiKhcV(mf^MhW1ZJxZym5eYDTgg1}yBQ9P}rGRTG$0j$YOHb!^n}Bc{ zvffYTc7#;WrF`=QIYbD0RCnGq?hil#i0-^SiOtp4L1pLTV6F!m@$wOmFDF*je?|Zt z+A#l)ZS z>_Z0{7`hye>su`=L!@WZ1Mzt*mrR7WK;@t21!z>xj`N$7imA zf%Re5D&o7c-H%1kO!H%Zx^s+1Ef#fc!vNk2*0kqr4oAtJ&ZoLMR`q!vWMD8YCBOO3 zPA1xTk1}ULMCDzqCn`-|0Zr@fzGi|s@C7LGslQt<0;oRE7Z*hZOV2nj0^)2zMh}!<#`;2iyBVuAocGx-VbHUG( zdCmmx{GD1*Uw^Bkv)(Gl6Yq5G(jX2iEIyY3Oa~2GfvtSn%J+NE32rC%`Ov%U8#}HQ zb9+s;N7;}Ae*Y1i$r?VGk}HetVPBSyfWoaxEiJqkRcof>52cLb*D5h4I^+Qx%M+2s zv;npflztVSn4uO*GHi&bldk(>SA$RgEls195QhD$uGN- zDX0lXXl8GaNq%wQ*PjG7nNT#E9YP3QCu0^r7{M|*ew?#dgh|5N*I@ib71hutCS4pW zt>P%{G3SaA7|#@=pLyJv*a>3d;$41!@S``c@C<1obUrtGhaPc<&SLNW`%POe2yTrt z>)Z&PSf zY$UP?b~3+X;8lyOuk^%*0Hpey+QS_(@RLai_VJO^FR#^7V}fc4`nV8wj7HDhz8$Ow zi(lHbY8-U{7SQ^Xpu|Z2;l^RD!;2n%SN6VZucZjei3<3ZRykuzTX;p(mT4$X{itVg zLrP%%)PchbDd#c}5+wlGXj;^Cn*ZTw8X`U<7qdj{H_jIm)^p;Q^hin>MMs6x5%bW! z`j@>Zv&#Itm|SW{a+QEy=`)Oa;Oa3r!B-DT!5^04OM4YSudY?NfCb!@CD4qWyrwRI zO&n1H<+N=2KoU>H6Y=)lF{Gta`SD6<5*CGE3Nqe{aAc%l8`zcPsqUeE=vcK`P8bMG zZxbkMg;-G5GyjsmdgE7gaNP*tjDm5G)h8j4NS&qXsaDuGS#Ggb0-tWuy8{&KU)w?e z|Khdd?DQ*q0^U85@7t{YdX2Gb04eD)hiSu`zl`=FU;T=#r8_&UAHfy$nVh}EA%1X{ zlYtukfj53&!ANJuM7Ho6$}cyIg_S@=42ic1S2}c;Nec~tbP>fFf8|WcaW;rfa*TJ& z=$&&MT;+kD;qe)3T*%OvBCcMwdh$_MSUtINe9e1*>{;TwV*?Ya+}pGVx7mn~y%cW1 z&r8^7g`@yVq=?=dr9TkDoRUKqq_$a`!w4)c=Ys)A9fki26OQ`$Vi|hvZYgS3(PQAy zz2sKk_@)e*7crQ-uBp5P? zHmwA$;WA}6{j|O!caHbI+_fpe9#&?#>$d56Fx-*IIzGZswk99||0Kkj35tA= zM(dx~4a6g6_k_~=w=ZzXhY`WCJJBbGSOwW^C$mj?5Wh#{H`J~><$$}4R_4~Nu(?O} z{SW6+Ws+$~t`D7)i zuML+YG%{FL^DWy0ki;%a_~hJa6m!Q@j?Zi=<+?_}nZfQCZ>hJ|NL|TjpA}{Yy$4H?&3fQ_ z(nNY<{S0b-0J&cQ1%?b$ZrO1cUIk^xk^hq3md3HcqM->|#(LV_y!KTSt)EckmaK%y2NywFiSydAg9usq5%nwk_&rSoX+J4RBFL)&z<-b1~xvgiF;?A#=#edo0p+i zIV;BBQ+_uK*4;MN)|@?KE>l%F&H%V;zb*Ib|EuUZ^0$WarY#5J7VN6dlFR$E0#v_p zIHoVF>iS38uRtAtB7L5mX%AZsQ@q4Qj5S0e2yi+|(>iOC1QHsNG zVv#;wPLx%q-hRqN_xHCw!;4brjqhD-4tL^ON0;5Vs0(2&*uwz(VzJ4U&z>;Evd1IJH# z%nViZC~pmo165#;ZzrrJGaAMgtkd>#om(1*54~(VT_nc<(~1FL%Z9grxPB@W6Eubj z!&%ipX1F7V3x^SJsOsKF-~h;zTyVk46lh>iPpMwfTz%2)7!|#1Q;<+C#P+@W zFbeEe7MOdC5M+Ra_VM>sObr%?`4`XYfYy*_HitckN_M%i>)W`?{XL`Z`}__vl~&xI zrkA(4>XRr{sY>kr`bXqw01S2mU|>f0A}pR`lF2!u?Fh|p_P!)7%Bi8h8#HcpO|ywb zRMp`Mr8Xh`50@wSIhfjA`$5fg2iU7$vI5FwoE>&PLWU=4GS#f-;wmQ51L!`JSc7a3 zRVJEM2_S9v@v`W6wT6{G_r;=za$S;a!3#)Ntn|>6yuF@VWwxoP$&c1xf@Db-zA&JHvt-yZeocL%5ek^GE zz{lY^abW{%fPcL3W};qY>>YnI(h<4GJccJi7?2Rc%^_)E%c6HP89$-8uwBLIdJVDKfa-?^6TH{r<$P+{8m0!+kgAuZA}r z1xfYh6-okJT;aOmGCYcd3F@@-or`-vNr8by{6CkxZnjKVT!x;(-1UNOGNj&2LaXdg z2m)x-3YIe_f}8<}REeAu8|y7d0fp>tS_hJlH`Ggc&Y`l{+J|{n6ILE~SToEl+-;=(S=!9^6M;L4bv}2l$1p74Vc#$jB;_D1WAS z8Ljdjnq-0@>&+MvmW0G}ZW}BY*KaXLfs!aPAj?OqJT&`CJz5E5F%*8W50g#25ga^x zuXqW3f(2kUi?SPb%J*)Ga1nY`wvEH;MRhs69zOeSTHW^PTE=upXyX5&f;DzoCR*8L z9bhxIAd=4`doC`ceyGLcfPfGPmThU8OKg&PyLK`Acd&drcqY2nd;wp-TN8$ac1dpX zb3Sx&F{DZk2;R)?AFaWUMNR7b9QVhZW{6-{UxVB7Jnb9O2PriOBDVu1QAd493RrZ* zn)rpu1kP1~>99p7InTag=;un3aa+S1{{Ikc7p1_CHar=K1As=tvQmj1I(fAPDRmxs zkB{?&vFGMNUcPN05ze1U1>e>-B5XJjQ53GDM)qmpILx8GzsaO&6MSM1Z^V6^*5DHw zkeA;W?!7jDCA{gpu!`?8me(GP<9_fkj_8Ilip2~p5q-*bsi(W!-(wxSmgK|ydY*MB z7v!!6xD7XxMIP|QQk&ETIpu>vKauxm2rAugPu4G9T()163<%?^Jq+fn?80=A_h!2+ z*Cq*K9MW2XFBwY5q6y1SA&bWX6jo+$^K*`|evNDge7UOp20Tb22P{N|@Jd~+O7I4z zpS1$V(iNGr94b1ARX;xbangPqp0l}2z9cbxk}}4nh92|U3bR>C9FRX8=uggK88+j3 z!BU(E+rJ7mCLzC!5~n&flz_v^V$7RoTM304M`h zkY7SZM|(emTWw$^hxW0uJz*?3$RJ*~L9`*Oo!@S-pisKsiGd z%W4~H^Y9NrAggmhR_DIMO33#jBG_*dyO`5;=)30og7338(}IV;q9+M-djt<(;w2E` zDOrApxYWDDXe1K3iVv8hFaQ`(RhfKy%*eM#dSJq?`<~r!8X)Dl1@;l=^low_PlO3~ zuPDW)CAa1%cQ&M$I;#t0XJM5J5N!jPg=sLmJZUNw;IK!Ym~!F3y3~p_QHk@2qY@Uq znDD>H#2o8PIi~L}F2y-G+gHqVm;eYh5eTameyLTRh5`ZWoqbkQQhBti>Q8DB$lMJay zEqR5Yy z+?v4FvPT{W??#}OE>wtZ6xI}qsCuOWf#Vxk%3Y8mv%>}s0lb<~&FpLCWkRgb-!9uY z6=+;C4j!Q=A%8tJeA3<~Iv0q%A_uQ~E>oh|x-YTdl`4@xp=OVXmp-$JCZnfu)*cZvsy}&6^;#53EHlrt{zA1tv`2@D+73RYY@MEn3^dC3Hw0#-QVo%u! z!R0X&Q-mGO9?t=wDn=QQ`N}iC;G66f&pEcSzK}8xZ+&@9Kmw3tKa7d%FsY9N2RVhG zh1eD4Z-PKMx@NE}r!dWxk@p?~RUEshmwd;!>^u@xL8X?s`wx>oef6E`}(-mW=y)#}^kpd_20bFsE| z5bW1WaB-O*Wha1exW{q;fXDY}Wb?po@PZz8ijEJjp%Q3pwh7vxZV?ZbJZnatTyYaf zzp&%1v+VBgZC5t1sn3~#vLY|u-aPH!m9jnB8XfOj3Q7eIq+;FpS`Wy|?LsQn+!!MT zy;0TId;|LOBjk3A*VeO>c*NPI=e^V{`xywnovCHcg^rU_N z+fPMc%o&wYR^>m&D%Hs^R6) zse)pz!_~Pmmur4urL{ROY}_7D**2?XhN?B6M%}a1Q($4#gwNUTIw1GEjX~JSRBYWT ze?7nHuE2Xbo zrZgB9Kdx|Y8CWM!)@MMPl%@S}?KZQ|i7S+1Yp^`Vl-@(jR=EBPiHeSD7)y_ApJRC5 z1=JHWP+BB9+W>(e9-+I6Y!6c0Q1WOv;bwHFAT@pk-RLLw^hVI>D_^V3$p6VIf zZc7QMcsBf48+1Wy@NTbZi31X6I80h9mz?JM5bz;Dp!Dp~q14+A$3Cv*x&|Y zLK=O_z-DO)3yphK*|t5d4Xs5SVgin$JTO!=(OvJY-0kY)Tg@a+z8&QC(cYZ&U|9CL!K7+n zjUoI|IG1+n5}E3j1R-NTM>MUm5()uwix-=!#wk6^-k5Ux!suEvF< zH1uNAv6m*xP^^0isV%^5f*fDoBFh+Q)8e{FQn~(s3+sboEUUER%{Q#<9pZaYdT;&K zI}+G|jkI(OsKp2?7xlr}aRNI4)9(`@0n`1mUc~~|5W_Fu9AWS2z6L z@}fA**|J0`hA1dXeWNsF>P zPh8T>4;rW@G&f@thM;9^=ch#h9cC=99F_4<)Bp*!sQ$VqrT#~U&9@5toRPH!%3e3Z z=x1uUetzjfQQaE;WbIQ|g?s2w(C#XFg(GxxueMuzTBG^cD_!VT%_7rjAiOd^oL%X? z5DfDjJ`Rj&f+<{+++B`VN`nD$7TdIFs<5?+%jMz2@sB$QEF8hBk4-usFl6Pnnjz`7 zZ^Tr=?CTopc&bF$n;{NUw;2kX?#CR8_G4`hqwNCs%rrMt)-jyBFMXZJ)?dy2y+gk> zTNcz62o^Z&Qd4n@u1+Cimp#O*fv+$~ERt(EadP&j-8!@NtHwKs8I-F6xdVn6w@zJm zOrt)9)W3(c+aLUwysA6NOUh?t0}D{Y(phr+Xv4o zuwSQLfWAr%*FA`NX@IYHDSWwl?Gdt;G0joOAM)hs&SQexow9_yF4JygnOv6FSaGf_ z;<_?CmrlZ$sewO%I%i)TJa-G|sKnLH*Kr}AhK=Vy_n_47VMZZ0qKH7?B>I_rwfiq4 z*tb3rCXntf`VN?0F4V@_5H^P}r`q=S+r)ULDA+z%pCLr)ue>*}JCS_reu{rt@gOhP zK#~$ErvLD$aqC^@fUImivio;G&I*h(Fy3a}d>a0O`o{8@)Et42$v|_0u{C=9Zb)qM zjZ-4O3kQ*C+sMbY6D8R)lU%tRZ#M4ZCfGS9OKQ|4l^4xyt4zx>7~AC9Gksg7-9&L- z0<-#4(%7Rx+9*=EJ=gtmSr##!VjlKW#C~KPecoXVV5IVkWcYhNs-FVv-k3sUAe8x2 z3^H6hRN;Dq@HiT@1Uuu5<#NLz(GlQ4bbD}HC*4SXN`tx&Y1v_uY0)rmj#&kTts_8t zx?ftH{U%%21(W=Vx`HTfSQ}gRS)4@HZvEVKOLD5qj4h&8fB#-$J*FeCn~uY|B-y5{ z5a3CCU+YJ^YI)AK1~FhrGFKYGtO8rhmxam5=!3m-NR0w5K_Cd#;T zyJy*PKEjg~x^ErGBAGzGtWyMD&|6itgL$g@bam*=8?%%HffGJivl&W}$#h_T*=T(+ z<@_|W{`}gJ`&rDxff@S0YV@C;m`GHcN@`sBe0cp7NpOvTjsGRfH*cVv(Joi>-PvR|5=*P1B?;tQ4VWZ^u z;d~NXBQ8Gs5s5LXn!L-qa7lrdljL-|;T5Ey*vqbXR+CY1ZF8w{?xLD?1%p8VK1>iy z8CC}>%NUq`I@bl)psG)fcQ^Nqge+3N9dW4H((a!i6Yi*>QOO)evWAb;t&AG)YFB}g zvIbR?12oVms{t=bg((xNR<&*Eq($qOqkLI_nS>ekg-M#oZw(sP2yp)Xt$R=p8}H5@ z3q3oWVtqejb)NbK4+OMg%Xhi(*GpPu`&UMxCU%7ERMWb8(84{`HDc5cM69f1J#y`V z(ba-{(oxq-4|7VNG?d_ZbZX0(f|$(ELcd`*7jAHYhJ7}%t)IS?$kBRdQb<%l=Ask(w1rGnmU>M)OlUA`W=a) zLtO@qD!r!{sQLD+yegraIu4%}Olz4(`*;39AgLeGwp1SZengSx)~-vjYydz?5xtSJ zr~Pc>3V2!X+H_qH*Hw{4`TMr3;eL-PIE9urw&`9|Oux(7-fmf5aH4c3(Wd9)w%9Mz zAZy|w_bp%)D`36MYqm(GcbTBUujsoPn5C#+@vomwIKC%I6;+^=kx2iQqPKj8UwvxOR1e7NtVpplwjtpgPPf?+7osji;kr3a zU1=0ozvz}x?;P&!y4dd1O5X)r|FH5?R>ewX5$Hg6KB2XZKe;BUl`QXWzv!CWeUjx* zrCk!UA2XXvrEQxYFk?9FXI?b}z_46=&uFqIu+cZc%1pp8%MBxX+$zLtNCCc&+WOu$ zhLT(uBG6&7c~V}pQ)Yx~Q#PM@(7^0KF+1)lEeZm9Xw0%+5! zjT^s+0CN4xOMu;1OHVnaT&52kg%o4T8B1#08I7mTVauip8t2OyY)3uXmw%rN;HvMI z9}*ic!=~|ZL{zIY*IR(yxfVjZDA{O55tsySD7){qwHWkaPuXHDO_GWWgFTzlWp7gL^J=XGM^UUq~ZTyD@DMhaay_; zV%gUgHgPfdY5L7a$jvaK`;Cn0&&4jpUmW029jV{=uC~OYn6lI~PO9XW??{|DEt-1n z&Ot}1f*X;|X!{D?ADBb#?g{mk@FYi#fN5Xps8cWFJyqUoK;%d*P?L^pJ;_0R{-TfNk0S{sR68lg6ophj=Tb3(wJcq9((53vpuLT%`Za(uMP)}{1yXOgU&5g3K)+Sm!z%-*ImidM@h7|6`^&j!7nJ9cV^UMS*Uv2j2EeWWBk&+9!*!$DDC>m=6qKaQq=dgm02ePe2E@?3I0;a|GHE zac=epE+jJwY=5#r9 zafKv|dC`Nn_}$_3^K->(DQd~0yBmPvANqiBHq2Xc%wrS z7D_Q0m+u7%8(Co1HVPk8>pKoqIY(5lG{Y>=Ow3*ty3O0AEc*Jye%B9C1^Y7~JcyRG z)WQ05-bn>Z8EECmnR;4}Oi<)mZ@o~U_fz&+YDX})VCAUI@!ncw=wgeBF0x+3e;hb^ z+wH1hCwq+aSyl#pFXhhxyAANQlqkZ;>i%yUXLBW4)*W8yTCV$pbk zy)4El84gu~za3YYdQ1(~u%rgKk2Dc{7D&Eap|`0|STqdUsA}!8%VS<)nw)$1wf8jH!F*qr*-D_HN>94juh#6LZD>dIv(5 zn=u+0zhm$=O@4biDFL#FT+&}p@J(}II?gecjoE!H4Nl@0KC7bzp&z056szw+3elm_ zcM4@`fJB&GAm8;BZA+GRbXGTWz?8Xv?5z{s+F{D=bY8T5Yzf}2FRTCIFBGIfcq&o>@|e`q zZx8*%Dci3xh3=ct;3P%V2$Q9srMlbLZ}uf=S+%*8Oc$P$J-JG_KD+%vFe@3Dmt6+8 z=5y)a3xd(`+j!Yp03!lFf7S`eu*%8Td*<74HW@fxBmHPmXJ7&SQR=vmJ_{Xa*FEv% zJ{kbH^V>RBnvM3>17^Lk=)S<3OSpaAC%N^K@2%QHw=ZVvm@LEU^k$C1NDUQNrM24C zA#nPm1Ll2E&}gq!M%*ls%JucTc-ik`Y5-%2fmq^gm~eEbGcO`Or6@2`frETB>TvZL zY_fB_vVO)hN%v^G!7?AykFW`lV1IB|60$2Yf?WaeUbgqt=dgVs`vS^Pri{I-v_+?n zk*v#uPHEakL%;H&dhT+ZiKF;wMF?qopR5XEE&)5OvDwxrY(XiYpJK4>F`FUQZGE4%SCJ>-3|ulQVcgC8B+roH=%MaPyFr1w#ABJ zyN2QXNSB6VdJ=qndyYo((D+UwKQYcho8@6lb(-N<`wVfnldg>p>K4p1&3d@=)Rp@s zpHTN}d5*g9dh&BZ5X7#4lgsOIue_xZ@es>aD~u*Qn)*4TvD&Krg#EPerq$L=LR;PG z4YAZPEsYRoX1IECQ&rhhr8kH2#~H$+t|rIdZyHDh1M z;dDxJh**VTZDwqcuimZ>!T%U~lh&s-PO3%L3mDoFX7}9Roa?EZ&b<*lGby^l0^|Y% zVc~KtHmUI|VqE>qATB5ZjqH=YnWPGhR0yr;_cz~hu~V2Dl!>gMaX7=gH!P0{L378dv!BZZ1*lcLBrZzmBVlLX2y6qKgpu6agT+ziI7HfejTSbIyfE*Z=F z2+@1m@@b*E{?+u>+$yXeAnz%zb!sfDSrJ|2mGS&#BFQ#msk`h5bB1JE=X~zH>DEWH zR@jtS&Am)8m)OrGUxMGXl+{|+Id{sw)l=_cm*yLp$o(44P}~!$A9Q>=S_gOd!Pfh0 zqi)6Tl9hf!%dUQoqgyM$6K-(UZsUX>llenEJW!Z|g^D8oLi5mi4TWDNq+R2yi-Meq zH*S*IhvRfh*Info!l!eQcmX1Tdg+vxzBlM#>iNSC(r%{B7{7wmkrqYMInK-WgteG1 z_at5MPXB&Y(%2}f6Y=J9(aZXs*M=M3__cMUevLWXB{MT{P;6`8ffHy-vdi(U^}ZkD z(aPlbsx5#_uvA2doXTqq!`lKYV4W9w#Vw<`n)LLCDoIB#55_LPziXdwK>*a)jP7N0 z=AbUb*h4iy)K`x>{gF;xVnzIAg1S6yJx=>yvDJ8b-=Exd+noCC7iiqpojoOybJ8V&?YXAc#j?jp-Hf{VF7_H{uXVd>G#9 z?86f0a0GtWF&AFMLjMj=QtaE4Q11?z^!k~O?RW4(GgrN2_j1pn%{54O+Mv3Z)z8!! z;@Qqk>mR{Tgzv|Nb=aiG2zy{z-T{d|Hcq8jg^gK75C~dB0BRv5aR#cLVB4+?c{SJ@_-C?Sm;o<2j7Y z;}}6xFxA=b_qn~pAkWay%_Z#Qvx!hG$KEqsYaYNi?EIk9R z@z+n6=G}?zHk)ge**|02R2U4mwIs*l-?WvJzPfI;rYYA zBBv`2T@fDG&eQq*9WrS4&CJNQ_S9ws(<@~VF-rLbB=G2dNe}hIfEqGJ6C4$aAH{)@ zE?4&K7N^23->gLE!1<|(n{jS#2_k7B)Q$^v)-L)SmAoPQmw{BhIQ$_;D6W1pl1H$r zBy;>O+DG39%vGydu>C5@QP8p?QJHUNd-M(U`|ZB{Esh|Jj3(~!1^oU+tABEB)mvb$o5|)K zX)Ngpf@;?9^tT&+>#61wG{!sn`nUpwKe<#B$D3{X^u+NILb0lTzj$R_C78rg=F$u{ zSK=7o)L;SX*H1>Da;a_Xu6{Kt$7PznOsE$+1RvY@qP6nAMtFLa74%adY6vNeSKC~f zf`NmHv1eT|v<~Cu7TL9unsj*5j??!prGtkk99vkbqv-p`8VR2*Ftis~bL+H>UNcS) zQPjCjITo_x9i*Kk`KIWMf`Suv*QN&ku4PAcd4a-v@ps^spkAho{PXf#EBf}xbJ8z% zP#2SBsenNys06@KW|DhX6;LfM3OL;_IB-}th3kFw9Fq4Gofgq?*$y9G}8K~{+y7V|r=tale=*4^p|+AbZF>TNsa zx0A&^@Hl-5nxI=Ql`Nxs39prHIP$j0?{iSeK>0q<3{tXg{IC-Gq2z8@#05Ug}4tsXpl}C%U2Q8iBuVQb1}WN2|Hv1$2ot-+`eE%;+|5HM)XPRyvqKu zUO%gMIc!K!OZC;3ajwJs>C(}uv(#z-!;uWmj6M5vhtYXYTOF?I5d^iEmv{(_FLV&@!noN+<$5wCMq1`hJuGzi+6hfb zrl)dnj=j@i_J}^Og61vnh?#D1R(4n>;j@rRTra;7apPo2W zeWX17%uCS~3}J1Bg>p$=zvEb@E5)$;S1;B&Cy$)$H$F_uokb$SmL9N$<7W{VE|8I zoq$lm;blOVRRaryQs6a#2MR(D^9V1y6ycAk|3HdKhF#$K4-0nC$ra8mEqjNNUv~XP z=9^(|`z}pEvQE^|8C@;mF@(-;eVG%?}j|=p~i@+ z?L~F|xe|Bw=1J-C*SS3Xfx7))@!*LZ3!g?0p;ovO7cqS64$G=&6L(g>oUR$d`hM=s zl2|g=Ut(ubY_wgc~sT7#YE z@hSrE_zz&A947t^*2cTW1%7-kX12o!j$j0K+2BiU&h!NQ1aiU?&s}>Cai1W8*fyQ( zmGzS=un9S1H}^MzP3s{JgWr z5D>CTASax%yubkM6)dtz22y+jKaOh8J$L0|JR|Df3J1@ zsQiZ1*FV1h|9Y8$F}OeD!q31W_V2a++h6fw$o6{O4WZF(dXuZrtZ) z{O4VN7w7Nd{EsvHZ{++WW8>%aNE z|39#T95hZ_YYR`f4+x415bw^_O++i!bc!k7Bzh6 tFF+dooX67g|MK=bh;deh;cG-f#Mzs9^A4Ek0`Fa8@O1TaS?83{1OPwr*F^vT literal 0 HcmV?d00001 From a0f482ad720a771de1082c40f1ff274d702a7e5b Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Sat, 22 Jun 2024 18:20:12 +0000 Subject: [PATCH 13/32] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- content/6_Advanced/SCC.mdx | 50 ++++++++++++++-------------- content/6_Advanced/SCC.problems.json | 6 ++-- 2 files changed, 28 insertions(+), 28 deletions(-) diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index 4302674ebc..84bcb6e1a8 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -283,7 +283,7 @@ After identifying the SCCs, we check for consistency. Specifically, we need to e 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](https://en.wikipedia.org/wiki/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 +For example, in the formula $ (\lnot x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2) \land (x_1 \lor \lnot x_3) $, the implication graph would have edges $(\lnot x_1 \rightarrow \lnot x_2), (x_1 \rightarrow x_2), (x_1 \rightarrow \lnot x_2), (\lnot x_1 \rightarrow \lnot x_3), (x_2 \rightarrow x_1), (\lnot x_2 \rightarrow \lnot x_1), (x_2 \rightarrow \lnot x_1)$ and $(x_3 \rightarrow x_1)$. @@ -306,12 +306,12 @@ Below is the implementation of the solution for the 2-SAT problem, utilizing the ```cpp struct TwoSatSolver { - int n_vars; - int n_vertices; - vector> adj, adj_t; - vector used; - vector order, comp; - vector assignment; + int n_vars; + int n_vertices; + vector> adj, adj_t; + vector used; + vector order, comp; + vector assignment; TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { order.reserve(n_vertices); @@ -413,12 +413,12 @@ using namespace std; // BeginCodeSnip{2SAT} struct TwoSatSolver { - int n_vars; - int n_vertices; - vector> adj, adj_t; - vector used; - vector order, comp; - vector assignment; + int n_vars; + int n_vertices; + vector> adj, adj_t; + vector used; + vector order, comp; + vector assignment; TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { order.reserve(n_vertices); @@ -495,17 +495,17 @@ struct TwoSatSolver { // EndCodeSnip int main() { - int n, m; - cin >> n >> m; - TwoSatSolver solver(m); - - for (int i = 1; i <= n; i++) { - int tops1, tops2; - char pref1, pref2; - cin >> pref1 >> tops1 >> pref2 >> tops2; - tops1--, tops2--; - solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); - } + int n, m; + cin >> n >> m; + TwoSatSolver solver(m); + + for (int i = 1; i <= n; i++) { + int tops1, tops2; + char pref1, pref2; + cin >> pref1 >> tops1 >> pref2 >> tops2; + tops1--, tops2--; + solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); + } if (!solver.solve()) { cout << "IMPOSSIBLE" << '\n'; @@ -522,7 +522,7 @@ int main() { ## Problems - diff --git a/content/6_Advanced/SCC.problems.json b/content/6_Advanced/SCC.problems.json index 42a19ea33c..10f9e55e3b 100644 --- a/content/6_Advanced/SCC.problems.json +++ b/content/6_Advanced/SCC.problems.json @@ -142,5 +142,91 @@ "kind": "none" } } + ], + "2SAT": [ + { + "uniqueId": "cf-1475F", + "name": "Unusual Matrix", + "url": "https://codeforces.com/contest/1475/problem/F", + "source": "CF", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-776D", + "name": "The Door Problem", + "url": "https://codeforces.com/contest/776/problem/D", + "source": "CF", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT", "DSU", "DFS"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cc-HKRMAN", + "name": "Hackerman", + "url": "https://www.codechef.com/LTIME95A/problems/HKRMAN", + "source": "CC", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT", "DSU", "Sliding Window", "Greedy"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "kattis-illumination", + "name": "Illumination", + "url": "https://open.kattis.com/problems/illumination", + "source": "Kattis", + "difficulty": "Easy", + "isStarred": false, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "ac-CoprimeSolitaire", + "name": "Coprime Solitaire", + "url": "https://atcoder.jp/contests/abc210/tasks/abc210_f", + "source": "AC", + "difficulty": "Normal", + "isStarred": true, + "tags": ["2SAT"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-1903F", + "name": "Babysitting", + "url": "https://codeforces.com/problemset/problem/1903/F", + "source": "CF", + "difficulty": "Hard", + "isStarred": true, + "tags": ["2SAT", "Binary Search", "Trees"], + "solutionMetadata": { + "kind": "internal" + } + }, + { + "uniqueId": "cf-1089H", + "name": "Harder Satisfiability", + "url": "https://codeforces.com/problemset/problem/1089/H", + "source": "CF", + "difficulty": "Hard", + "isStarred": true, + "tags": ["2SAT", "DFS"], + "solutionMetadata": { + "kind": "internal" + } + } ] } diff --git a/content/6_Advanced/graph.png b/content/6_Advanced/graph.png new file mode 100644 index 0000000000000000000000000000000000000000..ff03f8cb4d6f4acb261a13016adfcc011b75d9fe GIT binary patch literal 28069 zcmeFac{r5q{{}2sqbNmEXhB63F=ZRo(`uO{*|KE|G0E20hEyt|D6)<=`<8tlQuZ;j zZ!@DX48~~2HfDRT>Gyqp%klp6{{0^P@$|?sGxt5$^;yo(d7jtZ^Xn#;w{P3GjfaP4 z`_(J|+~DEiWpn=%5&*v$bP=xs|J&kw$d|D0qO z{?>!PbK~FH`TskAu=mh?HhmUi&lnp{q4nq#*UWv0 zP9d<@sxW(s?mr>!8?L_O8!0o9IU2?w*X)!x$UMHK8J$PGVZ|-B@7^}S!)U3*1C)oC zY3y}0`t0v-5~*ca{b1Y$TY9I3cL2_Rn229*45Up8LaS?jy!1YupEs%oxRb0y@*A)x zKTNokNan2wc*v9tCf{x~kC^i@c3y8(?Sxp!$iJGaY6Vr;ASe>O22H~0>Z<`!4 zga$#NdTU!YX_a2AdHu=8g%*(=v#K@K8_6C5OWJ)TpUgot{Yo36ib1OaA2h@JZ;w zcX1N(B_X_sT9mi+!jr1_vc@jkr9NE_9SeVOIP+d(lNoArfcUmJWTyAUy^6tGmFs>`-oG1 zgdD{aG0&$SI;GE8?5}697Ngv88sRH7*w7`TILFxq5oQaNc|mPNOgZ`GtczN(l`mMO zhb=Lreq{T>C{Y~Dn-9A7CC+POZvf~A5jQ}{-s}nB6S{fg)sy5ku*SrG6nmweR?Q;A z37^C`0pni7!TZvlq^Z^~f5kWTVv%ebhLnxce;_A@XupsGX&@P6_7p$-{u;F!LE7eQ z$F9g4(VYz6n$ogE=U$#*2#BQd1=Tm6pKLRzZ?X%<2k++X`Jw?*q@0frnZ&n+H(laN zV2nz&U(eau0>qN=3t_leP;X?4vMuS_!oE-rgFspR$*w{&s)*AGFgsdVV0FuZl)#1s zTTJD+_xM>FM*C;|;8jR!S&z1-`5wECuTomrhpif}H!5JE^JW+p1<4^k5>d6R;M`WO z*?ALW)k*l4W+eVs?B(#LtZma*kpf;tdp6~k!v#-cgNDjp%sOBluqzAD)d91p47W{& z+fb(HA#+!?SEIq|(XhHB%Ss#A(vX#pa$ZYe>vhH2-%h|0UE9UvQ7#SSRGx?#kW@)k zUg^?Xcuz#=vW%5<$N+n-6nz(GOL5}FY-+{7vyeX z|0f1k_u4JK9#I%MKKV%>`SL*!*Sa9C5gs~{TX<8Czq*c`eto$p?*h>s`z8jtnT^yQ z+;pkTysS5GiYX3T%{OOY9Qxh#X~|}K8R><)Ef?I8uJBqq2Cfe&s=s&*&1rtnpNcQ1 z&s(6itF+IEgMtI?b?g~` z8qi@GnGSM7v8|#%3*t{i%%)d8x+7~FGPXvdKo_&9I7(Pxg7lN!V1v624VFd85d| zIFQFDh*}sgc|&Ru=Uu0j`I$~X!h!5uccY1ZOmU%=)0BppapXj8+4Q5+f)07_xh?W zAXS<<9k8$mw6!X913d{zPa=Xh`BN^*H?tMg5LYSN&1&PfCl+k~kzssvoJ~h@=r`w` zl|c8{t02D-w~Ok_%a_>EISUzxiD^qawnm($EPs-NsM;@kf)HRjp24z^$Fz~Rl;U~%mp-x(*;o}4j zivYobs(Q-(Q-(gbd-#AY_W2wV%M)>&U)>X?v)nLq0xqpR z5-=f=_6Z&si~_mhn>wpIdsdl^$e?w`1;=V4mk!I(ulRz`_5FTqVn#L4T^|%WV?S#v z%E8D7SiSWL^YNM1L#(wbLKp*&Ep;^*I|Vr)yw0GYIeAL#VkB!J6}_2{w*FGw24(-o z$l#ZsKA)dy0ZVceq_pA8Jy0*cihyoRxa$r6EY6vgw7K^q_(t#(<=gLb*b1R_f@0i4 zTm%vFD`Da(EIV2Piuox=U(5Q$$$RqTNIB-D-E}z?u24ebu0ca{4H}eL3tJ`kB+(}0 z4d_&iMhdsnHw1K6$2?xmzddt2$t&TQj>Z+ngQU9KvZ--^S{5q3- zXYHL+?2i~O;)n*FNXk_Z1d#@xx;gQJEcMl%D7^o$Z7OH8m~*_y!yRW)-!FVEg5U&*_zy95|u%cV>Zj3R?2vI2mZcL zbQ^m{4LK?k{o3cSRd~LABZozS#Dy+81#>c#SWyQ8Ea8c$0O`uaf98{s7TiiJ2Etjk zGxi*)v_hXKA&*8Ju3AI~pf~|DS-7gY29BT3S<ez^ z4NEZ=POTEI$?ZSPOBDm*(u%-~>{RUQ%d#~~i$+nh zL3iQf&D51_XanMRw7srLMaWYw9Fqia%;>HlC@*4{PS&aBl0kK>I-yG`h=$ zcUOu6FFPcgQZR`PZ)v7tT*Ia#B!&W=%2Uw*7N3)o1;UBG?OHpo> z>7o+{RHg#5uUVi(zp>^nL&p}r(pu!$B{i#sa9nWot0iq|p|ldzD`YdjR6*Vd**mZf zAHu3Rw^xNEyF!K|gTJFcrosr$bdjM>^&cudEI)KWb>Mm}2h$VKv=Okl8 zT&Hv08d;*tX_vT(+b5;#DJ+^;aQ4;r);A=fZxCBAb@{-OdghE8JY#bp+hkVWX-Q$~ zB0xoT<|vb@_w~uwxvQuKQqZn1_Ck2m1b=DDd`a#e+5p7t^bTbbIvp`dd#vS4hJA#u zPx`3qO{XvUW$%eHvAv<>Qp*bq`6ZExWX~e)zVv(AE?8rR8`mm`*DPxL{KP7I@akta z{ELHeFJR86O3LXJW)G#iPZK&WjdXoB>*Au>Ttth&dA?0aV4sY(eyY3VFy1XRVn zCdqI}D7O1|sLeNbt)$5k^LXD+e81NUu9fAU>z6tFN>z^>|63{9`quviKfY3XCCfG1 z)oEq$OC1uk6ac=Q2+!_aI*>$qC*A*AbJv)HnGgHBJ@dN}Y&Ffd$6Y<+ux+S-Va6IN zbZzuP_WpGDCyQx35j`S8>~u6AkGQ3Ggy;w34UeSt21+O<6d=`_jF7Bd2ZqqPWr8k~ zx$2=21z$tTQgH?J?`mORJZ4FKtFNMToi_!&Qiva-Rp(#sbQk;8)7+YVBS3LanHevi z_6hloz*>5`ZiKhcV(mf^MhW1ZJxZym5eYDTgg1}yBQ9P}rGRTG$0j$YOHb!^n}Bc{ zvffYTc7#;WrF`=QIYbD0RCnGq?hil#i0-^SiOtp4L1pLTV6F!m@$wOmFDF*je?|Zt z+A#l)ZS z>_Z0{7`hye>su`=L!@WZ1Mzt*mrR7WK;@t21!z>xj`N$7imA zf%Re5D&o7c-H%1kO!H%Zx^s+1Ef#fc!vNk2*0kqr4oAtJ&ZoLMR`q!vWMD8YCBOO3 zPA1xTk1}ULMCDzqCn`-|0Zr@fzGi|s@C7LGslQt<0;oRE7Z*hZOV2nj0^)2zMh}!<#`;2iyBVuAocGx-VbHUG( zdCmmx{GD1*Uw^Bkv)(Gl6Yq5G(jX2iEIyY3Oa~2GfvtSn%J+NE32rC%`Ov%U8#}HQ zb9+s;N7;}Ae*Y1i$r?VGk}HetVPBSyfWoaxEiJqkRcof>52cLb*D5h4I^+Qx%M+2s zv;npflztVSn4uO*GHi&bldk(>SA$RgEls195QhD$uGN- zDX0lXXl8GaNq%wQ*PjG7nNT#E9YP3QCu0^r7{M|*ew?#dgh|5N*I@ib71hutCS4pW zt>P%{G3SaA7|#@=pLyJv*a>3d;$41!@S``c@C<1obUrtGhaPc<&SLNW`%POe2yTrt z>)Z&PSf zY$UP?b~3+X;8lyOuk^%*0Hpey+QS_(@RLai_VJO^FR#^7V}fc4`nV8wj7HDhz8$Ow zi(lHbY8-U{7SQ^Xpu|Z2;l^RD!;2n%SN6VZucZjei3<3ZRykuzTX;p(mT4$X{itVg zLrP%%)PchbDd#c}5+wlGXj;^Cn*ZTw8X`U<7qdj{H_jIm)^p;Q^hin>MMs6x5%bW! z`j@>Zv&#Itm|SW{a+QEy=`)Oa;Oa3r!B-DT!5^04OM4YSudY?NfCb!@CD4qWyrwRI zO&n1H<+N=2KoU>H6Y=)lF{Gta`SD6<5*CGE3Nqe{aAc%l8`zcPsqUeE=vcK`P8bMG zZxbkMg;-G5GyjsmdgE7gaNP*tjDm5G)h8j4NS&qXsaDuGS#Ggb0-tWuy8{&KU)w?e z|Khdd?DQ*q0^U85@7t{YdX2Gb04eD)hiSu`zl`=FU;T=#r8_&UAHfy$nVh}EA%1X{ zlYtukfj53&!ANJuM7Ho6$}cyIg_S@=42ic1S2}c;Nec~tbP>fFf8|WcaW;rfa*TJ& z=$&&MT;+kD;qe)3T*%OvBCcMwdh$_MSUtINe9e1*>{;TwV*?Ya+}pGVx7mn~y%cW1 z&r8^7g`@yVq=?=dr9TkDoRUKqq_$a`!w4)c=Ys)A9fki26OQ`$Vi|hvZYgS3(PQAy zz2sKk_@)e*7crQ-uBp5P? zHmwA$;WA}6{j|O!caHbI+_fpe9#&?#>$d56Fx-*IIzGZswk99||0Kkj35tA= zM(dx~4a6g6_k_~=w=ZzXhY`WCJJBbGSOwW^C$mj?5Wh#{H`J~><$$}4R_4~Nu(?O} z{SW6+Ws+$~t`D7)i zuML+YG%{FL^DWy0ki;%a_~hJa6m!Q@j?Zi=<+?_}nZfQCZ>hJ|NL|TjpA}{Yy$4H?&3fQ_ z(nNY<{S0b-0J&cQ1%?b$ZrO1cUIk^xk^hq3md3HcqM->|#(LV_y!KTSt)EckmaK%y2NywFiSydAg9usq5%nwk_&rSoX+J4RBFL)&z<-b1~xvgiF;?A#=#edo0p+i zIV;BBQ+_uK*4;MN)|@?KE>l%F&H%V;zb*Ib|EuUZ^0$WarY#5J7VN6dlFR$E0#v_p zIHoVF>iS38uRtAtB7L5mX%AZsQ@q4Qj5S0e2yi+|(>iOC1QHsNG zVv#;wPLx%q-hRqN_xHCw!;4brjqhD-4tL^ON0;5Vs0(2&*uwz(VzJ4U&z>;Evd1IJH# z%nViZC~pmo165#;ZzrrJGaAMgtkd>#om(1*54~(VT_nc<(~1FL%Z9grxPB@W6Eubj z!&%ipX1F7V3x^SJsOsKF-~h;zTyVk46lh>iPpMwfTz%2)7!|#1Q;<+C#P+@W zFbeEe7MOdC5M+Ra_VM>sObr%?`4`XYfYy*_HitckN_M%i>)W`?{XL`Z`}__vl~&xI zrkA(4>XRr{sY>kr`bXqw01S2mU|>f0A}pR`lF2!u?Fh|p_P!)7%Bi8h8#HcpO|ywb zRMp`Mr8Xh`50@wSIhfjA`$5fg2iU7$vI5FwoE>&PLWU=4GS#f-;wmQ51L!`JSc7a3 zRVJEM2_S9v@v`W6wT6{G_r;=za$S;a!3#)Ntn|>6yuF@VWwxoP$&c1xf@Db-zA&JHvt-yZeocL%5ek^GE zz{lY^abW{%fPcL3W};qY>>YnI(h<4GJccJi7?2Rc%^_)E%c6HP89$-8uwBLIdJVDKfa-?^6TH{r<$P+{8m0!+kgAuZA}r z1xfYh6-okJT;aOmGCYcd3F@@-or`-vNr8by{6CkxZnjKVT!x;(-1UNOGNj&2LaXdg z2m)x-3YIe_f}8<}REeAu8|y7d0fp>tS_hJlH`Ggc&Y`l{+J|{n6ILE~SToEl+-;=(S=!9^6M;L4bv}2l$1p74Vc#$jB;_D1WAS z8Ljdjnq-0@>&+MvmW0G}ZW}BY*KaXLfs!aPAj?OqJT&`CJz5E5F%*8W50g#25ga^x zuXqW3f(2kUi?SPb%J*)Ga1nY`wvEH;MRhs69zOeSTHW^PTE=upXyX5&f;DzoCR*8L z9bhxIAd=4`doC`ceyGLcfPfGPmThU8OKg&PyLK`Acd&drcqY2nd;wp-TN8$ac1dpX zb3Sx&F{DZk2;R)?AFaWUMNR7b9QVhZW{6-{UxVB7Jnb9O2PriOBDVu1QAd493RrZ* zn)rpu1kP1~>99p7InTag=;un3aa+S1{{Ikc7p1_CHar=K1As=tvQmj1I(fAPDRmxs zkB{?&vFGMNUcPN05ze1U1>e>-B5XJjQ53GDM)qmpILx8GzsaO&6MSM1Z^V6^*5DHw zkeA;W?!7jDCA{gpu!`?8me(GP<9_fkj_8Ilip2~p5q-*bsi(W!-(wxSmgK|ydY*MB z7v!!6xD7XxMIP|QQk&ETIpu>vKauxm2rAugPu4G9T()163<%?^Jq+fn?80=A_h!2+ z*Cq*K9MW2XFBwY5q6y1SA&bWX6jo+$^K*`|evNDge7UOp20Tb22P{N|@Jd~+O7I4z zpS1$V(iNGr94b1ARX;xbangPqp0l}2z9cbxk}}4nh92|U3bR>C9FRX8=uggK88+j3 z!BU(E+rJ7mCLzC!5~n&flz_v^V$7RoTM304M`h zkY7SZM|(emTWw$^hxW0uJz*?3$RJ*~L9`*Oo!@S-pisKsiGd z%W4~H^Y9NrAggmhR_DIMO33#jBG_*dyO`5;=)30og7338(}IV;q9+M-djt<(;w2E` zDOrApxYWDDXe1K3iVv8hFaQ`(RhfKy%*eM#dSJq?`<~r!8X)Dl1@;l=^low_PlO3~ zuPDW)CAa1%cQ&M$I;#t0XJM5J5N!jPg=sLmJZUNw;IK!Ym~!F3y3~p_QHk@2qY@Uq znDD>H#2o8PIi~L}F2y-G+gHqVm;eYh5eTameyLTRh5`ZWoqbkQQhBti>Q8DB$lMJay zEqR5Yy z+?v4FvPT{W??#}OE>wtZ6xI}qsCuOWf#Vxk%3Y8mv%>}s0lb<~&FpLCWkRgb-!9uY z6=+;C4j!Q=A%8tJeA3<~Iv0q%A_uQ~E>oh|x-YTdl`4@xp=OVXmp-$JCZnfu)*cZvsy}&6^;#53EHlrt{zA1tv`2@D+73RYY@MEn3^dC3Hw0#-QVo%u! z!R0X&Q-mGO9?t=wDn=QQ`N}iC;G66f&pEcSzK}8xZ+&@9Kmw3tKa7d%FsY9N2RVhG zh1eD4Z-PKMx@NE}r!dWxk@p?~RUEshmwd;!>^u@xL8X?s`wx>oef6E`}(-mW=y)#}^kpd_20bFsE| z5bW1WaB-O*Wha1exW{q;fXDY}Wb?po@PZz8ijEJjp%Q3pwh7vxZV?ZbJZnatTyYaf zzp&%1v+VBgZC5t1sn3~#vLY|u-aPH!m9jnB8XfOj3Q7eIq+;FpS`Wy|?LsQn+!!MT zy;0TId;|LOBjk3A*VeO>c*NPI=e^V{`xywnovCHcg^rU_N z+fPMc%o&wYR^>m&D%Hs^R6) zse)pz!_~Pmmur4urL{ROY}_7D**2?XhN?B6M%}a1Q($4#gwNUTIw1GEjX~JSRBYWT ze?7nHuE2Xbo zrZgB9Kdx|Y8CWM!)@MMPl%@S}?KZQ|i7S+1Yp^`Vl-@(jR=EBPiHeSD7)y_ApJRC5 z1=JHWP+BB9+W>(e9-+I6Y!6c0Q1WOv;bwHFAT@pk-RLLw^hVI>D_^V3$p6VIf zZc7QMcsBf48+1Wy@NTbZi31X6I80h9mz?JM5bz;Dp!Dp~q14+A$3Cv*x&|Y zLK=O_z-DO)3yphK*|t5d4Xs5SVgin$JTO!=(OvJY-0kY)Tg@a+z8&QC(cYZ&U|9CL!K7+n zjUoI|IG1+n5}E3j1R-NTM>MUm5()uwix-=!#wk6^-k5Ux!suEvF< zH1uNAv6m*xP^^0isV%^5f*fDoBFh+Q)8e{FQn~(s3+sboEUUER%{Q#<9pZaYdT;&K zI}+G|jkI(OsKp2?7xlr}aRNI4)9(`@0n`1mUc~~|5W_Fu9AWS2z6L z@}fA**|J0`hA1dXeWNsF>P zPh8T>4;rW@G&f@thM;9^=ch#h9cC=99F_4<)Bp*!sQ$VqrT#~U&9@5toRPH!%3e3Z z=x1uUetzjfQQaE;WbIQ|g?s2w(C#XFg(GxxueMuzTBG^cD_!VT%_7rjAiOd^oL%X? z5DfDjJ`Rj&f+<{+++B`VN`nD$7TdIFs<5?+%jMz2@sB$QEF8hBk4-usFl6Pnnjz`7 zZ^Tr=?CTopc&bF$n;{NUw;2kX?#CR8_G4`hqwNCs%rrMt)-jyBFMXZJ)?dy2y+gk> zTNcz62o^Z&Qd4n@u1+Cimp#O*fv+$~ERt(EadP&j-8!@NtHwKs8I-F6xdVn6w@zJm zOrt)9)W3(c+aLUwysA6NOUh?t0}D{Y(phr+Xv4o zuwSQLfWAr%*FA`NX@IYHDSWwl?Gdt;G0joOAM)hs&SQexow9_yF4JygnOv6FSaGf_ z;<_?CmrlZ$sewO%I%i)TJa-G|sKnLH*Kr}AhK=Vy_n_47VMZZ0qKH7?B>I_rwfiq4 z*tb3rCXntf`VN?0F4V@_5H^P}r`q=S+r)ULDA+z%pCLr)ue>*}JCS_reu{rt@gOhP zK#~$ErvLD$aqC^@fUImivio;G&I*h(Fy3a}d>a0O`o{8@)Et42$v|_0u{C=9Zb)qM zjZ-4O3kQ*C+sMbY6D8R)lU%tRZ#M4ZCfGS9OKQ|4l^4xyt4zx>7~AC9Gksg7-9&L- z0<-#4(%7Rx+9*=EJ=gtmSr##!VjlKW#C~KPecoXVV5IVkWcYhNs-FVv-k3sUAe8x2 z3^H6hRN;Dq@HiT@1Uuu5<#NLz(GlQ4bbD}HC*4SXN`tx&Y1v_uY0)rmj#&kTts_8t zx?ftH{U%%21(W=Vx`HTfSQ}gRS)4@HZvEVKOLD5qj4h&8fB#-$J*FeCn~uY|B-y5{ z5a3CCU+YJ^YI)AK1~FhrGFKYGtO8rhmxam5=!3m-NR0w5K_Cd#;T zyJy*PKEjg~x^ErGBAGzGtWyMD&|6itgL$g@bam*=8?%%HffGJivl&W}$#h_T*=T(+ z<@_|W{`}gJ`&rDxff@S0YV@C;m`GHcN@`sBe0cp7NpOvTjsGRfH*cVv(Joi>-PvR|5=*P1B?;tQ4VWZ^u z;d~NXBQ8Gs5s5LXn!L-qa7lrdljL-|;T5Ey*vqbXR+CY1ZF8w{?xLD?1%p8VK1>iy z8CC}>%NUq`I@bl)psG)fcQ^Nqge+3N9dW4H((a!i6Yi*>QOO)evWAb;t&AG)YFB}g zvIbR?12oVms{t=bg((xNR<&*Eq($qOqkLI_nS>ekg-M#oZw(sP2yp)Xt$R=p8}H5@ z3q3oWVtqejb)NbK4+OMg%Xhi(*GpPu`&UMxCU%7ERMWb8(84{`HDc5cM69f1J#y`V z(ba-{(oxq-4|7VNG?d_ZbZX0(f|$(ELcd`*7jAHYhJ7}%t)IS?$kBRdQb<%l=Ask(w1rGnmU>M)OlUA`W=a) zLtO@qD!r!{sQLD+yegraIu4%}Olz4(`*;39AgLeGwp1SZengSx)~-vjYydz?5xtSJ zr~Pc>3V2!X+H_qH*Hw{4`TMr3;eL-PIE9urw&`9|Oux(7-fmf5aH4c3(Wd9)w%9Mz zAZy|w_bp%)D`36MYqm(GcbTBUujsoPn5C#+@vomwIKC%I6;+^=kx2iQqPKj8UwvxOR1e7NtVpplwjtpgPPf?+7osji;kr3a zU1=0ozvz}x?;P&!y4dd1O5X)r|FH5?R>ewX5$Hg6KB2XZKe;BUl`QXWzv!CWeUjx* zrCk!UA2XXvrEQxYFk?9FXI?b}z_46=&uFqIu+cZc%1pp8%MBxX+$zLtNCCc&+WOu$ zhLT(uBG6&7c~V}pQ)Yx~Q#PM@(7^0KF+1)lEeZm9Xw0%+5! zjT^s+0CN4xOMu;1OHVnaT&52kg%o4T8B1#08I7mTVauip8t2OyY)3uXmw%rN;HvMI z9}*ic!=~|ZL{zIY*IR(yxfVjZDA{O55tsySD7){qwHWkaPuXHDO_GWWgFTzlWp7gL^J=XGM^UUq~ZTyD@DMhaay_; zV%gUgHgPfdY5L7a$jvaK`;Cn0&&4jpUmW029jV{=uC~OYn6lI~PO9XW??{|DEt-1n z&Ot}1f*X;|X!{D?ADBb#?g{mk@FYi#fN5Xps8cWFJyqUoK;%d*P?L^pJ;_0R{-TfNk0S{sR68lg6ophj=Tb3(wJcq9((53vpuLT%`Za(uMP)}{1yXOgU&5g3K)+Sm!z%-*ImidM@h7|6`^&j!7nJ9cV^UMS*Uv2j2EeWWBk&+9!*!$DDC>m=6qKaQq=dgm02ePe2E@?3I0;a|GHE zac=epE+jJwY=5#r9 zafKv|dC`Nn_}$_3^K->(DQd~0yBmPvANqiBHq2Xc%wrS z7D_Q0m+u7%8(Co1HVPk8>pKoqIY(5lG{Y>=Ow3*ty3O0AEc*Jye%B9C1^Y7~JcyRG z)WQ05-bn>Z8EECmnR;4}Oi<)mZ@o~U_fz&+YDX})VCAUI@!ncw=wgeBF0x+3e;hb^ z+wH1hCwq+aSyl#pFXhhxyAANQlqkZ;>i%yUXLBW4)*W8yTCV$pbk zy)4El84gu~za3YYdQ1(~u%rgKk2Dc{7D&Eap|`0|STqdUsA}!8%VS<)nw)$1wf8jH!F*qr*-D_HN>94juh#6LZD>dIv(5 zn=u+0zhm$=O@4biDFL#FT+&}p@J(}II?gecjoE!H4Nl@0KC7bzp&z056szw+3elm_ zcM4@`fJB&GAm8;BZA+GRbXGTWz?8Xv?5z{s+F{D=bY8T5Yzf}2FRTCIFBGIfcq&o>@|e`q zZx8*%Dci3xh3=ct;3P%V2$Q9srMlbLZ}uf=S+%*8Oc$P$J-JG_KD+%vFe@3Dmt6+8 z=5y)a3xd(`+j!Yp03!lFf7S`eu*%8Td*<74HW@fxBmHPmXJ7&SQR=vmJ_{Xa*FEv% zJ{kbH^V>RBnvM3>17^Lk=)S<3OSpaAC%N^K@2%QHw=ZVvm@LEU^k$C1NDUQNrM24C zA#nPm1Ll2E&}gq!M%*ls%JucTc-ik`Y5-%2fmq^gm~eEbGcO`Or6@2`frETB>TvZL zY_fB_vVO)hN%v^G!7?AykFW`lV1IB|60$2Yf?WaeUbgqt=dgVs`vS^Pri{I-v_+?n zk*v#uPHEakL%;H&dhT+ZiKF;wMF?qopR5XEE&)5OvDwxrY(XiYpJK4>F`FUQZGE4%SCJ>-3|ulQVcgC8B+roH=%MaPyFr1w#ABJ zyN2QXNSB6VdJ=qndyYo((D+UwKQYcho8@6lb(-N<`wVfnldg>p>K4p1&3d@=)Rp@s zpHTN}d5*g9dh&BZ5X7#4lgsOIue_xZ@es>aD~u*Qn)*4TvD&Krg#EPerq$L=LR;PG z4YAZPEsYRoX1IECQ&rhhr8kH2#~H$+t|rIdZyHDh1M z;dDxJh**VTZDwqcuimZ>!T%U~lh&s-PO3%L3mDoFX7}9Roa?EZ&b<*lGby^l0^|Y% zVc~KtHmUI|VqE>qATB5ZjqH=YnWPGhR0yr;_cz~hu~V2Dl!>gMaX7=gH!P0{L378dv!BZZ1*lcLBrZzmBVlLX2y6qKgpu6agT+ziI7HfejTSbIyfE*Z=F z2+@1m@@b*E{?+u>+$yXeAnz%zb!sfDSrJ|2mGS&#BFQ#msk`h5bB1JE=X~zH>DEWH zR@jtS&Am)8m)OrGUxMGXl+{|+Id{sw)l=_cm*yLp$o(44P}~!$A9Q>=S_gOd!Pfh0 zqi)6Tl9hf!%dUQoqgyM$6K-(UZsUX>llenEJW!Z|g^D8oLi5mi4TWDNq+R2yi-Meq zH*S*IhvRfh*Info!l!eQcmX1Tdg+vxzBlM#>iNSC(r%{B7{7wmkrqYMInK-WgteG1 z_at5MPXB&Y(%2}f6Y=J9(aZXs*M=M3__cMUevLWXB{MT{P;6`8ffHy-vdi(U^}ZkD z(aPlbsx5#_uvA2doXTqq!`lKYV4W9w#Vw<`n)LLCDoIB#55_LPziXdwK>*a)jP7N0 z=AbUb*h4iy)K`x>{gF;xVnzIAg1S6yJx=>yvDJ8b-=Exd+noCC7iiqpojoOybJ8V&?YXAc#j?jp-Hf{VF7_H{uXVd>G#9 z?86f0a0GtWF&AFMLjMj=QtaE4Q11?z^!k~O?RW4(GgrN2_j1pn%{54O+Mv3Z)z8!! z;@Qqk>mR{Tgzv|Nb=aiG2zy{z-T{d|Hcq8jg^gK75C~dB0BRv5aR#cLVB4+?c{SJ@_-C?Sm;o<2j7Y z;}}6xFxA=b_qn~pAkWay%_Z#Qvx!hG$KEqsYaYNi?EIk9R z@z+n6=G}?zHk)ge**|02R2U4mwIs*l-?WvJzPfI;rYYA zBBv`2T@fDG&eQq*9WrS4&CJNQ_S9ws(<@~VF-rLbB=G2dNe}hIfEqGJ6C4$aAH{)@ zE?4&K7N^23->gLE!1<|(n{jS#2_k7B)Q$^v)-L)SmAoPQmw{BhIQ$_;D6W1pl1H$r zBy;>O+DG39%vGydu>C5@QP8p?QJHUNd-M(U`|ZB{Esh|Jj3(~!1^oU+tABEB)mvb$o5|)K zX)Ngpf@;?9^tT&+>#61wG{!sn`nUpwKe<#B$D3{X^u+NILb0lTzj$R_C78rg=F$u{ zSK=7o)L;SX*H1>Da;a_Xu6{Kt$7PznOsE$+1RvY@qP6nAMtFLa74%adY6vNeSKC~f zf`NmHv1eT|v<~Cu7TL9unsj*5j??!prGtkk99vkbqv-p`8VR2*Ftis~bL+H>UNcS) zQPjCjITo_x9i*Kk`KIWMf`Suv*QN&ku4PAcd4a-v@ps^spkAho{PXf#EBf}xbJ8z% zP#2SBsenNys06@KW|DhX6;LfM3OL;_IB-}th3kFw9Fq4Gofgq?*$y9G}8K~{+y7V|r=tale=*4^p|+AbZF>TNsa zx0A&^@Hl-5nxI=Ql`Nxs39prHIP$j0?{iSeK>0q<3{tXg{IC-Gq2z8@#05Ug}4tsXpl}C%U2Q8iBuVQb1}WN2|Hv1$2ot-+`eE%;+|5HM)XPRyvqKu zUO%gMIc!K!OZC;3ajwJs>C(}uv(#z-!;uWmj6M5vhtYXYTOF?I5d^iEmv{(_FLV&@!noN+<$5wCMq1`hJuGzi+6hfb zrl)dnj=j@i_J}^Og61vnh?#D1R(4n>;j@rRTra;7apPo2W zeWX17%uCS~3}J1Bg>p$=zvEb@E5)$;S1;B&Cy$)$H$F_uokb$SmL9N$<7W{VE|8I zoq$lm;blOVRRaryQs6a#2MR(D^9V1y6ycAk|3HdKhF#$K4-0nC$ra8mEqjNNUv~XP z=9^(|`z}pEvQE^|8C@;mF@(-;eVG%?}j|=p~i@+ z?L~F|xe|Bw=1J-C*SS3Xfx7))@!*LZ3!g?0p;ovO7cqS64$G=&6L(g>oUR$d`hM=s zl2|g=Ut(ubY_wgc~sT7#YE z@hSrE_zz&A947t^*2cTW1%7-kX12o!j$j0K+2BiU&h!NQ1aiU?&s}>Cai1W8*fyQ( zmGzS=un9S1H}^MzP3s{JgWr z5D>CTASax%yubkM6)dtz22y+jKaOh8J$L0|JR|Df3J1@ zsQiZ1*FV1h|9Y8$F}OeD!q31W_V2a++h6fw$o6{O4WZF(dXuZrtZ) z{O4VN7w7Nd{EsvHZ{++WW8>%aNE z|39#T95hZ_YYR`f4+x415bw^_O++i!bc!k7Bzh6 tFF+dooX67g|MK=bh;deh;cG-f#Mzs9^A4Ek0`Fa8@O1TaS?83{1OPwr*F^vT literal 0 HcmV?d00001 From 2563916de28c92545b74a6e638dd47a8f05b8e0d Mon Sep 17 00:00:00 2001 From: Rameez Parwez Date: Wed, 26 Jun 2024 10:11:59 +0530 Subject: [PATCH 22/32] ignore --- content/6_Advanced/SCC.mdx | 2 -- 1 file changed, 2 deletions(-) diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index 3cffbe8351..bd470c2da1 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -2,7 +2,6 @@ id: SCC title: 'Strongly Connected Components' author: Benjamin Qi, Dong Liu, Neo Wang, Rameez Parwez -author: Benjamin Qi, Dong Liu, Neo Wang, Rameez Parwez prerequisites: - toposort - BCC-2CC @@ -259,7 +258,6 @@ int main() { ## 2-SAT -### Resources ### Resources From 6f4671aa48daf4798d62db6d06484a610a0a9822 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Wed, 26 Jun 2024 04:43:22 +0000 Subject: [PATCH 23/32] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- content/6_Advanced/SCC.mdx | 310 +++++++++++++-------------- content/6_Advanced/SCC.problems.json | 6 +- 2 files changed, 156 insertions(+), 160 deletions(-) diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index bd470c2da1..4feac6c9b2 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -272,7 +272,7 @@ The 2-Satisfiability (2-SAT) problem is a specific type of [Boolean satisfiabili ## 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 -$$ +$$ (\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 $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. @@ -283,7 +283,7 @@ After identifying the SCCs, we check for consistency. Specifically, we need to e 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](https://en.wikipedia.org/wiki/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 +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. @@ -303,79 +303,77 @@ Below is the implementation of the solution for the 2-SAT problem, utilizing the ```cpp struct TwoSatSolver { - int n_vars; - int n_vertices; - vector> adj, adj_t; - vector used; - vector order, comp; - vector assignment; - - TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { - order.reserve(n_vertices); - } - void dfs1(int v) { - used[v] = true; - for (int u : adj[v]) { - if (!used[u]) - dfs1(u); - } - order.push_back(v); - } - - void dfs2(int v, int cl) { - comp[v] = cl; - for (int u : adj_t[v]) { - if (comp[u] == -1) - dfs2(u, cl); - } - } - - bool solve_2SAT() { - order.clear(); - used.assign(n_vertices, false); - for (int i = 0; i < n_vertices; ++i) { - if (!used[i]) - dfs1(i); - } - - comp.assign(n_vertices, -1); - for (int i = 0, j = 0; i < n_vertices; ++i) { - int v = order[n_vertices - i - 1]; - if (comp[v] == -1) - dfs2(v, j++); - } - - assignment.assign(n_vars, false); - for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) - return false; - assignment[i / 2] = comp[i] > comp[i + 1]; - } - return true; - } - - void add_disjunction(int a, bool na, int b, bool nb) { - // na and nb signify whether a and b are to be negated - a = 2 * a ^ na; - b = 2 * b ^ nb; - int neg_a = a ^ 1; - int neg_b = b ^ 1; - adj[neg_a].push_back(b); - adj[neg_b].push_back(a); - adj_t[b].push_back(neg_a); - adj_t[a].push_back(neg_b); - } - - static void example_usage() { - TwoSatSolver solver(3); // a, b, c - solver.add_disjunction(0, false, 1, true); // a v not b - solver.add_disjunction(0, true, 1, true); // not a v not b - solver.add_disjunction(1, false, 2, false); // b v c - solver.add_disjunction(0, false, 0, false); // a v a - assert(solver.solve_2SAT() == true); - auto expected = vector(True, False, True); - assert(solver.assignment == expected); - } + int n_vars; + int n_vertices; + vector> adj, adj_t; + vector used; + vector order, comp; + vector assignment; + + TwoSatSolver(int _n_vars) + : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), + adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), + assignment(n_vars) { + order.reserve(n_vertices); + } + void dfs1(int v) { + used[v] = true; + for (int u : adj[v]) { + if (!used[u]) dfs1(u); + } + order.push_back(v); + } + + void dfs2(int v, int cl) { + comp[v] = cl; + for (int u : adj_t[v]) { + if (comp[u] == -1) dfs2(u, cl); + } + } + + bool solve_2SAT() { + order.clear(); + used.assign(n_vertices, false); + for (int i = 0; i < n_vertices; ++i) { + if (!used[i]) dfs1(i); + } + + comp.assign(n_vertices, -1); + for (int i = 0, j = 0; i < n_vertices; ++i) { + int v = order[n_vertices - i - 1]; + if (comp[v] == -1) dfs2(v, j++); + } + + assignment.assign(n_vars, false); + for (int i = 0; i < n_vertices; i += 2) { + if (comp[i] == comp[i + 1]) return false; + assignment[i / 2] = comp[i] > comp[i + 1]; + } + return true; + } + + void add_disjunction(int a, bool na, int b, bool nb) { + // na and nb signify whether a and b are to be negated + a = 2 * a ^ na; + b = 2 * b ^ nb; + int neg_a = a ^ 1; + int neg_b = b ^ 1; + adj[neg_a].push_back(b); + adj[neg_b].push_back(a); + adj_t[b].push_back(neg_a); + adj_t[a].push_back(neg_b); + } + + static void example_usage() { + TwoSatSolver solver(3); // a, b, c + solver.add_disjunction(0, false, 1, true); // a v not b + solver.add_disjunction(0, true, 1, true); // not a v not b + solver.add_disjunction(1, false, 2, false); // b v c + solver.add_disjunction(0, false, 0, false); // a v a + assert(solver.solve_2SAT() == true); + auto expected = vector(True, False, True); + assert(solver.assignment == expected); + } }; ``` @@ -392,90 +390,88 @@ It is a straightforward 2SAT problem. Each topping corresponds to a variable. Wh using namespace std; struct TwoSatSolver { - int n_vars; - int n_vertices; - vector> adj, adj_t; - vector used; - vector order, comp; - vector assignment; - - TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) { - order.reserve(n_vertices); - } - void dfs1(int v) { - used[v] = true; - for (int u : adj[v]) { - if (!used[u]) - dfs1(u); - } - order.push_back(v); - } - - void dfs2(int v, int cl) { - comp[v] = cl; - for (int u : adj_t[v]) { - if (comp[u] == -1) - dfs2(u, cl); - } - } - - bool solve_2SAT() { - order.clear(); - used.assign(n_vertices, false); - for (int i = 0; i < n_vertices; ++i) { - if (!used[i]) - dfs1(i); - } - - comp.assign(n_vertices, -1); - for (int i = 0, j = 0; i < n_vertices; ++i) { - int v = order[n_vertices - i - 1]; - if (comp[v] == -1) - dfs2(v, j++); - } - - assignment.assign(n_vars, false); - for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) - return false; - assignment[i / 2] = comp[i] > comp[i + 1]; - } - return true; - } - - void add_disjunction(int a, int na, int b, int nb) { - // na and nb signify whether a and b are to be negated - a = 2 * a ^ na; - b = 2 * b ^ nb; - int neg_a = a ^ 1; - int neg_b = b ^ 1; - adj[neg_a].push_back(b); - adj[neg_b].push_back(a); - adj_t[b].push_back(neg_a); - adj_t[a].push_back(neg_b); - } + int n_vars; + int n_vertices; + vector> adj, adj_t; + vector used; + vector order, comp; + vector assignment; + + TwoSatSolver(int _n_vars) + : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), + adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), + assignment(n_vars) { + order.reserve(n_vertices); + } + void dfs1(int v) { + used[v] = true; + for (int u : adj[v]) { + if (!used[u]) dfs1(u); + } + order.push_back(v); + } + + void dfs2(int v, int cl) { + comp[v] = cl; + for (int u : adj_t[v]) { + if (comp[u] == -1) dfs2(u, cl); + } + } + + bool solve_2SAT() { + order.clear(); + used.assign(n_vertices, false); + for (int i = 0; i < n_vertices; ++i) { + if (!used[i]) dfs1(i); + } + + comp.assign(n_vertices, -1); + for (int i = 0, j = 0; i < n_vertices; ++i) { + int v = order[n_vertices - i - 1]; + if (comp[v] == -1) dfs2(v, j++); + } + + assignment.assign(n_vars, false); + for (int i = 0; i < n_vertices; i += 2) { + if (comp[i] == comp[i + 1]) return false; + assignment[i / 2] = comp[i] > comp[i + 1]; + } + return true; + } + + void add_disjunction(int a, int na, int b, int nb) { + // na and nb signify whether a and b are to be negated + a = 2 * a ^ na; + b = 2 * b ^ nb; + int neg_a = a ^ 1; + int neg_b = b ^ 1; + adj[neg_a].push_back(b); + adj[neg_b].push_back(a); + adj_t[b].push_back(neg_a); + adj_t[a].push_back(neg_b); + } }; int main() { - int n, m; - cin >> n >> m; - TwoSatSolver solver(m); - - for (int i = 1; i <= n; i++) { - int tops1, tops2; - char pref1, pref2; - cin >> pref1 >> tops1 >> pref2 >> tops2; - tops1--, tops2--; - solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); - } - - if (!solver.solve_2SAT()) { - cout << "IMPOSSIBLE" << '\n'; - } else { - for (int i = 0; i < m; i++) { - cout << (!solver.assignment[i] ? '+' : '-') << " \n"[i == m - 1]; - } - } + int n, m; + cin >> n >> m; + TwoSatSolver solver(m); + + for (int i = 1; i <= n; i++) { + int tops1, tops2; + char pref1, pref2; + cin >> pref1 >> tops1 >> pref2 >> tops2; + tops1--, tops2--; + solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); + } + + if (!solver.solve_2SAT()) { + cout << "IMPOSSIBLE" << '\n'; + } else { + for (int i = 0; i < m; i++) { + cout << (!solver.assignment[i] ? '+' : '-') << " \n"[i == m - 1]; + } + } } ``` @@ -484,7 +480,7 @@ int main() { ## Problems - + + +in-house explanation? -### Solution (Kosaraju's) + + +## Implementation + +**Time Complexity:** $\mathcal{O}(N+M)$ @@ -163,7 +165,7 @@ public class Main { -### Tarjan's Algorithm +## Tarjan's Algorithm @@ -171,94 +173,127 @@ public class Main { - + -### Solution (Tarjan's) +link to dpv in resources and just tell them to look at that, no way we're +beating that explanation - + +## Implementation + +**Time Complexity:** $\mathcal{O}(N+M)$ + + ```cpp -#include -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 - * Verification: https://cses.fi/problemset/task/1686/ - */ -struct SCC { - int N, ti = 0; - vector> adj; - vector disc, comp, st, comps; - void init(int _N) { - N = _N; - adj.resize(N), disc.resize(N), comp = vector(N, -1); - } - void ae(int x, int y) { adj[x].push_back(y); } - int dfs(int x) { - int low = disc[x] = ++ti; - st.push_back(x); // disc[y] != 0 -> in stack - for (int y : adj[x]) - if (comp[y] == -1) low = min(low, disc[y] ?: dfs(y)); - if (low == disc[x]) { // make new SCC, pop off stack until you find x - comps.push_back(x); - for (int y = -1; y != x;) comp[y = st.back()] = x, st.pop_back(); - } - return low; - } - void gen() { - for (int i = 0; i < N; i++) - if (!disc[i]) dfs(i); - reverse(begin(comps), end(comps)); - } +#include +#include +#include + +using std::cout; +using std::endl; +using std::vector; + +/** Takes in an adjacency list and calculates the SCCs of the graph. */ +class TarjanSolver { + private: + vector> rev_adj; + vector post; + vector comp; + + vector visited; + int timer = 0; + int id = 0; + + void fill_post(int at) { + visited[at] = true; + for (int n : rev_adj[at]) { + if (!visited[n]) { + fill_post(n); + } + } + post[at] = timer++; + } + + void find_comp(int at) { + visited[at] = true; + comp[at] = id; + for (int n : adj[at]) { + if (!visited[n]) { + find_comp(n); + } + } + } + + public: + const vector>& adj; + + TarjanSolver(const vector>& adj) + : adj(adj), + rev_adj(adj.size()), + post(adj.size()), + comp(adj.size()), + visited(adj.size()) { + vector nodes(adj.size()); + for (int n = 0; n < adj.size(); n++) { + nodes[n] = n; + for (int next : adj[n]) { + rev_adj[next].push_back(n); + } + } + + for (int n = 0; n < adj.size(); n++) { + if (!visited[n]) { + fill_post(n); + } + } + std::sort(nodes.begin(), nodes.end(), + [&](int n1, int n2) { return post[n1] > post[n2]; }); + + visited.assign(adj.size(), false); + for (int n : nodes) { + if (!visited[n]) { + find_comp(n); + id++; + } + } + } + + int comp_num() const { return id; } + + int get_comp(int n) const { return comp[n]; } }; int main() { - int n, m, a, b; - cin >> n >> m; - - SCC graph; - graph.init(n); - while (m--) { - cin >> a >> b; - graph.ae(--a, --b); - } - graph.gen(); - int ID[200000]{}; - int ids = 0; - for (int i = 0; i < n; i++) { - if (!ID[graph.comp[i]]) { ID[graph.comp[i]] = ++ids; } - } - cout << ids << '\n'; - for (int i = 0; i < n; i++) { - cout << ID[graph.comp[i]] << " \n"[i == n - 1]; - } + int planet_num; + int tele_num; + std::cin >> planet_num >> tele_num; + vector> adj(planet_num); + for (int t = 0; t < tele_num; t++) { + int from, to; + std::cin >> from >> to; + adj[--from].push_back(--to); + } + + TarjanSolver scc(adj); + cout << scc.comp_num() << '\n'; + for (int p = 0; p < planet_num - 1; p++) { + cout << scc.get_comp(p) + 1 << ' '; + } + cout << scc.get_comp(planet_num - 1) + 1 << endl; } ``` - -### Problems +## Problems -## 2-SAT - -### Resources +# 2-SAT @@ -266,322 +301,241 @@ int main() { -## Introduction -The 2-Satisfiability (2-SAT) problem is a specific type of [Boolean satisfiability problem](https://en.wikipedia.org/wiki/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)](https://en.wikipedia.org/wiki/Conjunctive_normal_form), 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 - -$$ -(\lnot x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2) \land (x_1 \lor \lnot x_3) -$$ -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)](https://en.wikipedia.org/wiki/Strongly_connected_component) 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. +## Explanation -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. +### Introduction -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](https://en.wikipedia.org/wiki/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. +The CSES problem already gives us a boolean formula in conjunctive normal form +(CNF) that consists of a series of logical OR clauses ANDed together like so: -For example, in the formula -$ +$$ (\lnot x_1 \lor x_2) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2) \land (x_1 \lor \lnot x_3) -$, the implication graph would have edges $(\lnot x_1 \rightarrow \lnot x_2), (x_1 \rightarrow x_2), (x_1 \rightarrow \lnot x_2), (\lnot x_1 \rightarrow \lnot x_3), (x_2 \rightarrow x_1), (\lnot x_2 \rightarrow \lnot x_1), (x_2 \rightarrow \lnot x_1)$ and $(x_3 \rightarrow x_1)$. -![](graph.png) -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. +$$ +Before we proceed, try linking this to graph theory. Hint: represent a variable +and its negation with two nodes. -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. +### Construction -## 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$. +Like the hint says, we can construct a graph with each variable having two +nodes: one for itself and one for its negation. We're going to try to proceed by +assigning each node a truth value. Note that the value of one of the variable's +nodes determines the other, since if we know the value of one node, the other is +the negation of that value. -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. +Now, for each clause $(a \lor b)$, we add two directed edges: +$\lnot a \rightarrow b$ and $\lnot b \rightarrow a$. What this means for us is +that if $a$ was false, then $b$ must be true, and vice versa. -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. +With these edges, an SCC implies a group of values that all have to have the +same truth value. - - -```cpp -struct TwoSatSolver { - int n_vars; - int n_vertices; - vector> adj, adj_t; - vector used; - vector order, comp; - vector assignment; - - TwoSatSolver(int _n_vars) - : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), - adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), - assignment(n_vars) { - order.reserve(n_vertices); - } +### Solving the Graph - // Depth-first search for the first pass in Kosaraju's algorithm - void dfs1(int v) { - used[v] = true; - for (int u : adj[v]) { - if (!used[u]) { dfs1(u); } - } - order.push_back( - v); // Append node to order list after visiting all reachable nodes - } +The only way for there to be an impossible assignment of truth values is if a +node and its negation are in the same SCC, since this means that a boolean and +its negation have to both be true, which is impossible. - // Depth-first search for the second pass in Kosaraju's algorithm - void dfs2(int v, int cl) { - comp[v] = cl; - for (int u : adj_t[v]) { - if (comp[u] == -1) { dfs2(u, cl); } - } - } - - bool solve() { - order.clear(); - used.assign(n_vertices, false); - for (int i = 0; i < n_vertices; ++i) { - if (!used[i]) { dfs1(i); } - } - - comp.assign(n_vertices, -1); - for (int i = 0, j = 0; i < n_vertices; ++i) { - int v = order[n_vertices - i - 1]; - if (comp[v] == -1) { dfs2(v, j++); } - } - - assignment.assign(n_vars, false); - for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) { - return false; // If variable and its negation are in the same - // component, unsatisfiable - } - assignment[i / 2] = - comp[i] > - comp[i + 1]; // Assign true/false based on component ids - } - return true; // Satisfiable - } - - void add_disjunction(int a, int na, int b, int nb) { - // na and nb signify whether a and b are to be negated - - comp.assign(n_vertices, -1); - for (int i = 0, j = 0; i < n_vertices; ++i) { - int v = order[n_vertices - i - 1]; - if (comp[v] == -1) { dfs2(v, j++); } - } +If the graph is consistent and there are no impossible configurations, we can +start assigning truth values, starting from the SCCs that have no outgoing edges +to other SCCs and proceeding backwards. With the initial SCCs, we set them all +to true. As for other SCCs, if a value has already been assigned due to its +negation being in a previously processed component, we have to assign all other +values in the component to that value. - assignment.assign(n_vars, false); - for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) { - return false; // If variable and its negation are in the same - // component, unsatisfiable - } - assignment[i / 2] = - comp[i] > - comp[i + 1]; // Assign true/false based on component ids - } - return true; // Satisfiable - } +Due to +[certain properties about the graph we've constructed](https://en.wikipedia.org/wiki/2-satisfiability#Strongly_connected_components), +we can guarantee that the resulting assignment of the variables does not have +any "true" SCCs leading to "false" SCCs. A proof of this is beyond the scope of +this module. - /* - 'add_disjunction' is responsible for adding a clause of the form (𝑎 ∨ 𝑏) to - the 2-SAT problem. In the context of 2-SAT, each clause specifies a logical - disjunction of two literals, and the task is to determine if there is a way - to assign truth values to the variables so that all clauses are satisfied. - The 'add_disjunction function translates each clause into implications and - updates the implication graph accordingly. - */ - void add_disjunction(int a, int na, int b, int nb) { - // na and nb signify whether a and b are to be negated - - // Convert variable index and negation to node index - a = 2 * a ^ na; - b = 2 * b ^ nb; - - // Get the negation node index - int neg_a = a ^ 1; - int neg_b = b ^ 1; - - // Add implication from negation - adj[neg_a].push_back(b); - adj[neg_b].push_back(a); - - // Add reverse implication for the transposed graph - adj_t[b].push_back(neg_a); - adj_t[a].push_back(neg_b); - } -}; +## Implementation -static void example_usage() { - TwoSatSolver solver(3); // a, b, c - solver.add_disjunction(0, false, 1, true); // a v not b - solver.add_disjunction(0, true, 1, true); // not a v not b - solver.add_disjunction(1, false, 2, false); // b v c - solver.add_disjunction(0, false, 0, false); // a v a - assert(solver.solve() == true); - auto expected = vector(True, False, True); - assert(solver.assignment == expected); -} -} -; -``` - - - +We use Tarjan's algorithm as it already provides us with a topological order to +process the nodes in. However, it is also possible to use Kosaraju's algorithm. -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. +**Time Complexity:** $\mathcal{O}(N+M)$ -## Solution -```cpp -#include -using namespace std; - -struct TwoSatSolver { - int n_vars; - int n_vertices; - vector> adj, adj_t; - vector used; - vector order, comp; - vector assignment; - - TwoSatSolver(int _n_vars) - : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), - adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), - assignment(n_vars) { - order.reserve(n_vertices); - } - - // Depth-first search for the first pass in Kosaraju's algorithm - void dfs1(int v) { - used[v] = true; - for (int u : adj[v]) { - if (!used[u]) { dfs1(u); } - } - order.push_back( - v); // Append node to order list after visiting all reachable nodes - } - - // Depth-first search for the second pass in Kosaraju's algorithm - void dfs2(int v, int cl) { - comp[v] = cl; - for (int u : adj_t[v]) { - if (comp[u] == -1) { dfs2(u, cl); } - } - } - - bool solve() { - order.clear(); - used.assign(n_vertices, false); - for (int i = 0; i < n_vertices; ++i) { - if (!used[i]) { dfs1(i); } - } - comp.assign(n_vertices, -1); - for (int i = 0, j = 0; i < n_vertices; ++i) { - int v = order[n_vertices - i - 1]; - if (comp[v] == -1) { dfs2(v, j++); } - } - - assignment.assign(n_vars, false); - for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) { - return false; // If variable and its negation are in the same - // component, unsatisfiable - } - assignment[i / 2] = - comp[i] > - comp[i + 1]; // Assign true/false based on component ids - } - return true; // Satisfiable - } - - void add_disjunction(int a, int na, int b, int nb) { - // na and nb signify whether a and b are to be negated - - comp.assign(n_vertices, -1); - for (int i = 0, j = 0; i < n_vertices; ++i) { - int v = order[n_vertices - i - 1]; - if (comp[v] == -1) { dfs2(v, j++); } - } +```cpp +#include +#include +#include + +using std::cout; +using std::endl; +using std::vector; + +// BeginCodeSnip{SCC Solver} +class TarjanSolver { + private: + vector> rev_adj; + vector post; + vector comp; + + vector visited; + int timer = 0; + int id = 0; + + void fill_post(int at) { + visited[at] = true; + for (int n : rev_adj[at]) { + if (!visited[n]) { + fill_post(n); + } + } + post[at] = timer++; + } + + void find_comp(int at) { + visited[at] = true; + comp[at] = id; + for (int n : adj[at]) { + if (!visited[n]) { + find_comp(n); + } + } + } + + public: + const vector>& adj; + TarjanSolver(const vector>& adj) + : adj(adj), + rev_adj(adj.size()), + post(adj.size()), + comp(adj.size()), + visited(adj.size()) { + vector nodes(adj.size()); + for (int n = 0; n < adj.size(); n++) { + nodes[n] = n; + for (int next : adj[n]) { + rev_adj[next].push_back(n); + } + } + + for (int n = 0; n < adj.size(); n++) { + if (!visited[n]) { + fill_post(n); + } + } + std::sort(nodes.begin(), nodes.end(), + [&](int n1, int n2) { return post[n1] > post[n2]; }); + + visited.assign(adj.size(), false); + for (int n : nodes) { + if (!visited[n]) { + find_comp(n); + id++; + } + } + } + + int comp_num() const { return id; } + + int get_comp(int n) const { return comp[n]; } +}; +// EndCodeSnip - assignment.assign(n_vars, false); - for (int i = 0; i < n_vertices; i += 2) { - if (comp[i] == comp[i + 1]) { - return false; // If variable and its negation are in the same - // component, unsatisfiable - } - assignment[i / 2] = - comp[i] > - comp[i + 1]; // Assign true/false based on component ids - } - return true; // Satisfiable - } +struct Clause { + int var1; // id of the first variable + bool neg1; // is it negated? + int var2; + bool neg2; +}; - /* - 'add_disjunction' is responsible for adding a clause of the form (𝑎 ∨ 𝑏) to - the 2-SAT problem. In the context of 2-SAT, each clause specifies a logical - disjunction of two literals, and the task is to determine if there is a way - to assign truth values to the variables so that all clauses are satisfied. - The 'add_disjunction function translates each clause into implications and - updates the implication graph accordingly. - */ - void add_disjunction(int a, int na, int b, int nb) { - // na and nb signify whether a and b are to be negated - - // Convert variable index and negation to node index - a = 2 * a ^ na; - b = 2 * b ^ nb; - - // Get the negation node index - int neg_a = a ^ 1; - int neg_b = b ^ 1; - - // Add implication from negation - adj[neg_a].push_back(b); - adj[neg_b].push_back(a); - - // Add reverse implication for the transposed graph - adj_t[b].push_back(neg_a); - adj_t[a].push_back(neg_b); - } +class SATSolver { + private: + vector> adj; + bool valid = true; + vector val; + + /** @return the negation of the variable v */ + int get_neg(int v) { + return v % 2 == 1 ? v - 1 : v + 1; + } + public: + SATSolver(const vector& clauses, int var_num) + : adj(2 * var_num), val(2 * var_num, -1) { + // 2 * var is the variable, while 2 * var + 1 is its negation + for (const Clause& c : clauses) { + // falseness of the first implies the truth of the second + adj[2 * c.var1 + !c.neg1].push_back(2 * c.var2 + c.neg2); + // and vice versa + adj[2 * c.var2 + !c.neg2].push_back(2 * c.var1 + c.neg1); + } + + TarjanSolver scc(adj); + // a list of all the components in the graph + vector> comps(scc.comp_num()); + for (int i = 0; i < 2 * var_num; i += 2) { + // do a node and its negation share the same component? + if (scc.get_comp(i) == scc.get_comp(i + 1)) { + valid = false; + return; + } + comps[scc.get_comp(i)].push_back(i); + comps[scc.get_comp(i + 1)].push_back(i + 1); + } + + /* + * because of how our tarjan solver works, starting from + * starting from comp 0 and going up process the graph + * in reverse topological order- neat, huh? + */ + for (const vector& comp : comps) { + int set_to = 1; // set all to true by default + // check if any values have had their negations set yet + for (int v : comp) { + if (val[get_neg(v)] != -1) { + set_to = !val[get_neg(v)]; + break; + } + } + + for (int v : comp) { + val[v] = set_to; + } + } + } + + bool is_valid() const { return valid; } + + bool get_var(int var) const { return val[2 * var]; } }; int main() { - int n, m; - cin >> n >> m; - TwoSatSolver solver(m); - - for (int i = 1; i <= n; i++) { - int tops1, tops2; - char pref1, pref2; - cin >> pref1 >> tops1 >> pref2 >> tops2; - tops1--, tops2--; - solver.add_disjunction(tops1, pref1 == '+', tops2, pref2 == '+'); - } - - if (!solver.solve()) { - cout << "IMPOSSIBLE" << '\n'; - } else { - for (int i = 0; i < m; i++) { - cout << (!solver.assignment[i] ? '+' : '-') << " \n"[i == m - 1]; - } - } + int req_num; + int topping_num; + std::cin >> req_num >> topping_num; + vector clauses(req_num); + for (Clause& c : clauses) { + char neg1, neg2; + std::cin >> neg1 >> c.var1 >> neg2 >> c.var2; + c.var1--; + c.var2--; + c.neg1 = neg1 == '-'; + c.neg2 = neg2 == '-'; + } + + SATSolver sat(clauses, topping_num); + if (!sat.is_valid()) { + cout << "IMPOSSIBLE" << endl; + } else { + for (int t = 0; t < topping_num; t++) { + cout << (sat.get_var(t) ? '+' : '-') << ' '; + } + cout << endl; + } } ``` + ## Problems - - - + From ec08f4718f680adfc0b6f8e8437aec56012041a1 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Thu, 27 Jun 2024 22:32:33 +0000 Subject: [PATCH 31/32] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- content/6_Advanced/SCC.mdx | 435 +++++++++++++++++-------------------- 1 file changed, 205 insertions(+), 230 deletions(-) diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index b85e079564..2c9fdd1949 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -198,91 +198,80 @@ using std::vector; /** Takes in an adjacency list and calculates the SCCs of the graph. */ class TarjanSolver { - private: - vector> rev_adj; - vector post; - vector comp; - - vector visited; - int timer = 0; - int id = 0; - - void fill_post(int at) { - visited[at] = true; - for (int n : rev_adj[at]) { - if (!visited[n]) { - fill_post(n); - } - } - post[at] = timer++; - } - - void find_comp(int at) { - visited[at] = true; - comp[at] = id; - for (int n : adj[at]) { - if (!visited[n]) { - find_comp(n); - } - } - } - - public: - const vector>& adj; - - TarjanSolver(const vector>& adj) - : adj(adj), - rev_adj(adj.size()), - post(adj.size()), - comp(adj.size()), - visited(adj.size()) { - vector nodes(adj.size()); - for (int n = 0; n < adj.size(); n++) { - nodes[n] = n; - for (int next : adj[n]) { - rev_adj[next].push_back(n); - } - } - - for (int n = 0; n < adj.size(); n++) { - if (!visited[n]) { - fill_post(n); - } - } - std::sort(nodes.begin(), nodes.end(), - [&](int n1, int n2) { return post[n1] > post[n2]; }); - - visited.assign(adj.size(), false); - for (int n : nodes) { - if (!visited[n]) { - find_comp(n); - id++; - } - } - } - - int comp_num() const { return id; } - - int get_comp(int n) const { return comp[n]; } + private: + vector> rev_adj; + vector post; + vector comp; + + vector visited; + int timer = 0; + int id = 0; + + void fill_post(int at) { + visited[at] = true; + for (int n : rev_adj[at]) { + if (!visited[n]) { fill_post(n); } + } + post[at] = timer++; + } + + void find_comp(int at) { + visited[at] = true; + comp[at] = id; + for (int n : adj[at]) { + if (!visited[n]) { find_comp(n); } + } + } + + public: + const vector> &adj; + + TarjanSolver(const vector> &adj) + : adj(adj), rev_adj(adj.size()), post(adj.size()), comp(adj.size()), + visited(adj.size()) { + vector nodes(adj.size()); + for (int n = 0; n < adj.size(); n++) { + nodes[n] = n; + for (int next : adj[n]) { rev_adj[next].push_back(n); } + } + + for (int n = 0; n < adj.size(); n++) { + if (!visited[n]) { fill_post(n); } + } + std::sort(nodes.begin(), nodes.end(), + [&](int n1, int n2) { return post[n1] > post[n2]; }); + + visited.assign(adj.size(), false); + for (int n : nodes) { + if (!visited[n]) { + find_comp(n); + id++; + } + } + } + + int comp_num() const { return id; } + + int get_comp(int n) const { return comp[n]; } }; int main() { - int planet_num; - int tele_num; - std::cin >> planet_num >> tele_num; - vector> adj(planet_num); - for (int t = 0; t < tele_num; t++) { - int from, to; - std::cin >> from >> to; - adj[--from].push_back(--to); - } - - TarjanSolver scc(adj); - cout << scc.comp_num() << '\n'; - for (int p = 0; p < planet_num - 1; p++) { - cout << scc.get_comp(p) + 1 << ' '; - } - cout << scc.get_comp(planet_num - 1) + 1 << endl; + int planet_num; + int tele_num; + std::cin >> planet_num >> tele_num; + vector> adj(planet_num); + for (int t = 0; t < tele_num; t++) { + int from, to; + std::cin >> from >> to; + adj[--from].push_back(--to); + } + + TarjanSolver scc(adj); + cout << scc.comp_num() << '\n'; + for (int p = 0; p < planet_num - 1; p++) { + cout << scc.get_comp(p) + 1 << ' '; + } + cout << scc.get_comp(planet_num - 1) + 1 << endl; } ``` @@ -372,164 +361,150 @@ using std::vector; // BeginCodeSnip{SCC Solver} class TarjanSolver { - private: - vector> rev_adj; - vector post; - vector comp; - - vector visited; - int timer = 0; - int id = 0; - - void fill_post(int at) { - visited[at] = true; - for (int n : rev_adj[at]) { - if (!visited[n]) { - fill_post(n); - } - } - post[at] = timer++; - } - - void find_comp(int at) { - visited[at] = true; - comp[at] = id; - for (int n : adj[at]) { - if (!visited[n]) { - find_comp(n); - } - } - } - - public: - const vector>& adj; - TarjanSolver(const vector>& adj) - : adj(adj), - rev_adj(adj.size()), - post(adj.size()), - comp(adj.size()), - visited(adj.size()) { - vector nodes(adj.size()); - for (int n = 0; n < adj.size(); n++) { - nodes[n] = n; - for (int next : adj[n]) { - rev_adj[next].push_back(n); - } - } - - for (int n = 0; n < adj.size(); n++) { - if (!visited[n]) { - fill_post(n); - } - } - std::sort(nodes.begin(), nodes.end(), - [&](int n1, int n2) { return post[n1] > post[n2]; }); - - visited.assign(adj.size(), false); - for (int n : nodes) { - if (!visited[n]) { - find_comp(n); - id++; - } - } - } - - int comp_num() const { return id; } - - int get_comp(int n) const { return comp[n]; } + private: + vector> rev_adj; + vector post; + vector comp; + + vector visited; + int timer = 0; + int id = 0; + + void fill_post(int at) { + visited[at] = true; + for (int n : rev_adj[at]) { + if (!visited[n]) { fill_post(n); } + } + post[at] = timer++; + } + + void find_comp(int at) { + visited[at] = true; + comp[at] = id; + for (int n : adj[at]) { + if (!visited[n]) { find_comp(n); } + } + } + + public: + const vector> &adj; + TarjanSolver(const vector> &adj) + : adj(adj), rev_adj(adj.size()), post(adj.size()), comp(adj.size()), + visited(adj.size()) { + vector nodes(adj.size()); + for (int n = 0; n < adj.size(); n++) { + nodes[n] = n; + for (int next : adj[n]) { rev_adj[next].push_back(n); } + } + + for (int n = 0; n < adj.size(); n++) { + if (!visited[n]) { fill_post(n); } + } + std::sort(nodes.begin(), nodes.end(), + [&](int n1, int n2) { return post[n1] > post[n2]; }); + + visited.assign(adj.size(), false); + for (int n : nodes) { + if (!visited[n]) { + find_comp(n); + id++; + } + } + } + + int comp_num() const { return id; } + + int get_comp(int n) const { return comp[n]; } }; // EndCodeSnip struct Clause { - int var1; // id of the first variable - bool neg1; // is it negated? - int var2; - bool neg2; + int var1; // id of the first variable + bool neg1; // is it negated? + int var2; + bool neg2; }; class SATSolver { - private: - vector> adj; - bool valid = true; - vector val; - - /** @return the negation of the variable v */ - int get_neg(int v) { - return v % 2 == 1 ? v - 1 : v + 1; - } - public: - SATSolver(const vector& clauses, int var_num) - : adj(2 * var_num), val(2 * var_num, -1) { - // 2 * var is the variable, while 2 * var + 1 is its negation - for (const Clause& c : clauses) { - // falseness of the first implies the truth of the second - adj[2 * c.var1 + !c.neg1].push_back(2 * c.var2 + c.neg2); - // and vice versa - adj[2 * c.var2 + !c.neg2].push_back(2 * c.var1 + c.neg1); - } - - TarjanSolver scc(adj); - // a list of all the components in the graph - vector> comps(scc.comp_num()); - for (int i = 0; i < 2 * var_num; i += 2) { - // do a node and its negation share the same component? - if (scc.get_comp(i) == scc.get_comp(i + 1)) { - valid = false; - return; - } - comps[scc.get_comp(i)].push_back(i); - comps[scc.get_comp(i + 1)].push_back(i + 1); - } - - /* - * because of how our tarjan solver works, starting from - * starting from comp 0 and going up process the graph - * in reverse topological order- neat, huh? - */ - for (const vector& comp : comps) { - int set_to = 1; // set all to true by default - // check if any values have had their negations set yet - for (int v : comp) { - if (val[get_neg(v)] != -1) { - set_to = !val[get_neg(v)]; - break; - } - } - - for (int v : comp) { - val[v] = set_to; - } - } - } - - bool is_valid() const { return valid; } - - bool get_var(int var) const { return val[2 * var]; } + private: + vector> adj; + bool valid = true; + vector val; + + /** @return the negation of the variable v */ + int get_neg(int v) { return v % 2 == 1 ? v - 1 : v + 1; } + + public: + SATSolver(const vector &clauses, int var_num) + : adj(2 * var_num), val(2 * var_num, -1) { + // 2 * var is the variable, while 2 * var + 1 is its negation + for (const Clause &c : clauses) { + // falseness of the first implies the truth of the second + adj[2 * c.var1 + !c.neg1].push_back(2 * c.var2 + c.neg2); + // and vice versa + adj[2 * c.var2 + !c.neg2].push_back(2 * c.var1 + c.neg1); + } + + TarjanSolver scc(adj); + // a list of all the components in the graph + vector> comps(scc.comp_num()); + for (int i = 0; i < 2 * var_num; i += 2) { + // do a node and its negation share the same component? + if (scc.get_comp(i) == scc.get_comp(i + 1)) { + valid = false; + return; + } + comps[scc.get_comp(i)].push_back(i); + comps[scc.get_comp(i + 1)].push_back(i + 1); + } + + /* + * because of how our tarjan solver works, starting from + * starting from comp 0 and going up process the graph + * in reverse topological order- neat, huh? + */ + for (const vector &comp : comps) { + int set_to = 1; // set all to true by default + // check if any values have had their negations set yet + for (int v : comp) { + if (val[get_neg(v)] != -1) { + set_to = !val[get_neg(v)]; + break; + } + } + + for (int v : comp) { val[v] = set_to; } + } + } + + bool is_valid() const { return valid; } + + bool get_var(int var) const { return val[2 * var]; } }; int main() { - int req_num; - int topping_num; - std::cin >> req_num >> topping_num; - vector clauses(req_num); - for (Clause& c : clauses) { - char neg1, neg2; - std::cin >> neg1 >> c.var1 >> neg2 >> c.var2; - c.var1--; - c.var2--; - c.neg1 = neg1 == '-'; - c.neg2 = neg2 == '-'; - } - - SATSolver sat(clauses, topping_num); - if (!sat.is_valid()) { - cout << "IMPOSSIBLE" << endl; - } else { - for (int t = 0; t < topping_num; t++) { - cout << (sat.get_var(t) ? '+' : '-') << ' '; - } - cout << endl; - } + int req_num; + int topping_num; + std::cin >> req_num >> topping_num; + vector clauses(req_num); + for (Clause &c : clauses) { + char neg1, neg2; + std::cin >> neg1 >> c.var1 >> neg2 >> c.var2; + c.var1--; + c.var2--; + c.neg1 = neg1 == '-'; + c.neg2 = neg2 == '-'; + } + + SATSolver sat(clauses, topping_num); + if (!sat.is_valid()) { + cout << "IMPOSSIBLE" << endl; + } else { + for (int t = 0; t < topping_num; t++) { + cout << (sat.get_var(t) ? '+' : '-') << ' '; + } + cout << endl; + } } ``` From 5e42624c38be0ffae08dadbe7b0ff6ee9452f2e6 Mon Sep 17 00:00:00 2001 From: Rameez Parwez Date: Fri, 28 Jun 2024 05:43:53 +0530 Subject: [PATCH 32/32] removed graph.png --- content/6_Advanced/graph.png | Bin 28069 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 content/6_Advanced/graph.png diff --git a/content/6_Advanced/graph.png b/content/6_Advanced/graph.png deleted file mode 100644 index ff03f8cb4d6f4acb261a13016adfcc011b75d9fe..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 28069 zcmeFac{r5q{{}2sqbNmEXhB63F=ZRo(`uO{*|KE|G0E20hEyt|D6)<=`<8tlQuZ;j zZ!@DX48~~2HfDRT>Gyqp%klp6{{0^P@$|?sGxt5$^;yo(d7jtZ^Xn#;w{P3GjfaP4 z`_(J|+~DEiWpn=%5&*v$bP=xs|J&kw$d|D0qO z{?>!PbK~FH`TskAu=mh?HhmUi&lnp{q4nq#*UWv0 zP9d<@sxW(s?mr>!8?L_O8!0o9IU2?w*X)!x$UMHK8J$PGVZ|-B@7^}S!)U3*1C)oC zY3y}0`t0v-5~*ca{b1Y$TY9I3cL2_Rn229*45Up8LaS?jy!1YupEs%oxRb0y@*A)x zKTNokNan2wc*v9tCf{x~kC^i@c3y8(?Sxp!$iJGaY6Vr;ASe>O22H~0>Z<`!4 zga$#NdTU!YX_a2AdHu=8g%*(=v#K@K8_6C5OWJ)TpUgot{Yo36ib1OaA2h@JZ;w zcX1N(B_X_sT9mi+!jr1_vc@jkr9NE_9SeVOIP+d(lNoArfcUmJWTyAUy^6tGmFs>`-oG1 zgdD{aG0&$SI;GE8?5}697Ngv88sRH7*w7`TILFxq5oQaNc|mPNOgZ`GtczN(l`mMO zhb=Lreq{T>C{Y~Dn-9A7CC+POZvf~A5jQ}{-s}nB6S{fg)sy5ku*SrG6nmweR?Q;A z37^C`0pni7!TZvlq^Z^~f5kWTVv%ebhLnxce;_A@XupsGX&@P6_7p$-{u;F!LE7eQ z$F9g4(VYz6n$ogE=U$#*2#BQd1=Tm6pKLRzZ?X%<2k++X`Jw?*q@0frnZ&n+H(laN zV2nz&U(eau0>qN=3t_leP;X?4vMuS_!oE-rgFspR$*w{&s)*AGFgsdVV0FuZl)#1s zTTJD+_xM>FM*C;|;8jR!S&z1-`5wECuTomrhpif}H!5JE^JW+p1<4^k5>d6R;M`WO z*?ALW)k*l4W+eVs?B(#LtZma*kpf;tdp6~k!v#-cgNDjp%sOBluqzAD)d91p47W{& z+fb(HA#+!?SEIq|(XhHB%Ss#A(vX#pa$ZYe>vhH2-%h|0UE9UvQ7#SSRGx?#kW@)k zUg^?Xcuz#=vW%5<$N+n-6nz(GOL5}FY-+{7vyeX z|0f1k_u4JK9#I%MKKV%>`SL*!*Sa9C5gs~{TX<8Czq*c`eto$p?*h>s`z8jtnT^yQ z+;pkTysS5GiYX3T%{OOY9Qxh#X~|}K8R><)Ef?I8uJBqq2Cfe&s=s&*&1rtnpNcQ1 z&s(6itF+IEgMtI?b?g~` z8qi@GnGSM7v8|#%3*t{i%%)d8x+7~FGPXvdKo_&9I7(Pxg7lN!V1v624VFd85d| zIFQFDh*}sgc|&Ru=Uu0j`I$~X!h!5uccY1ZOmU%=)0BppapXj8+4Q5+f)07_xh?W zAXS<<9k8$mw6!X913d{zPa=Xh`BN^*H?tMg5LYSN&1&PfCl+k~kzssvoJ~h@=r`w` zl|c8{t02D-w~Ok_%a_>EISUzxiD^qawnm($EPs-NsM;@kf)HRjp24z^$Fz~Rl;U~%mp-x(*;o}4j zivYobs(Q-(Q-(gbd-#AY_W2wV%M)>&U)>X?v)nLq0xqpR z5-=f=_6Z&si~_mhn>wpIdsdl^$e?w`1;=V4mk!I(ulRz`_5FTqVn#L4T^|%WV?S#v z%E8D7SiSWL^YNM1L#(wbLKp*&Ep;^*I|Vr)yw0GYIeAL#VkB!J6}_2{w*FGw24(-o z$l#ZsKA)dy0ZVceq_pA8Jy0*cihyoRxa$r6EY6vgw7K^q_(t#(<=gLb*b1R_f@0i4 zTm%vFD`Da(EIV2Piuox=U(5Q$$$RqTNIB-D-E}z?u24ebu0ca{4H}eL3tJ`kB+(}0 z4d_&iMhdsnHw1K6$2?xmzddt2$t&TQj>Z+ngQU9KvZ--^S{5q3- zXYHL+?2i~O;)n*FNXk_Z1d#@xx;gQJEcMl%D7^o$Z7OH8m~*_y!yRW)-!FVEg5U&*_zy95|u%cV>Zj3R?2vI2mZcL zbQ^m{4LK?k{o3cSRd~LABZozS#Dy+81#>c#SWyQ8Ea8c$0O`uaf98{s7TiiJ2Etjk zGxi*)v_hXKA&*8Ju3AI~pf~|DS-7gY29BT3S<ez^ z4NEZ=POTEI$?ZSPOBDm*(u%-~>{RUQ%d#~~i$+nh zL3iQf&D51_XanMRw7srLMaWYw9Fqia%;>HlC@*4{PS&aBl0kK>I-yG`h=$ zcUOu6FFPcgQZR`PZ)v7tT*Ia#B!&W=%2Uw*7N3)o1;UBG?OHpo> z>7o+{RHg#5uUVi(zp>^nL&p}r(pu!$B{i#sa9nWot0iq|p|ldzD`YdjR6*Vd**mZf zAHu3Rw^xNEyF!K|gTJFcrosr$bdjM>^&cudEI)KWb>Mm}2h$VKv=Okl8 zT&Hv08d;*tX_vT(+b5;#DJ+^;aQ4;r);A=fZxCBAb@{-OdghE8JY#bp+hkVWX-Q$~ zB0xoT<|vb@_w~uwxvQuKQqZn1_Ck2m1b=DDd`a#e+5p7t^bTbbIvp`dd#vS4hJA#u zPx`3qO{XvUW$%eHvAv<>Qp*bq`6ZExWX~e)zVv(AE?8rR8`mm`*DPxL{KP7I@akta z{ELHeFJR86O3LXJW)G#iPZK&WjdXoB>*Au>Ttth&dA?0aV4sY(eyY3VFy1XRVn zCdqI}D7O1|sLeNbt)$5k^LXD+e81NUu9fAU>z6tFN>z^>|63{9`quviKfY3XCCfG1 z)oEq$OC1uk6ac=Q2+!_aI*>$qC*A*AbJv)HnGgHBJ@dN}Y&Ffd$6Y<+ux+S-Va6IN zbZzuP_WpGDCyQx35j`S8>~u6AkGQ3Ggy;w34UeSt21+O<6d=`_jF7Bd2ZqqPWr8k~ zx$2=21z$tTQgH?J?`mORJZ4FKtFNMToi_!&Qiva-Rp(#sbQk;8)7+YVBS3LanHevi z_6hloz*>5`ZiKhcV(mf^MhW1ZJxZym5eYDTgg1}yBQ9P}rGRTG$0j$YOHb!^n}Bc{ zvffYTc7#;WrF`=QIYbD0RCnGq?hil#i0-^SiOtp4L1pLTV6F!m@$wOmFDF*je?|Zt z+A#l)ZS z>_Z0{7`hye>su`=L!@WZ1Mzt*mrR7WK;@t21!z>xj`N$7imA zf%Re5D&o7c-H%1kO!H%Zx^s+1Ef#fc!vNk2*0kqr4oAtJ&ZoLMR`q!vWMD8YCBOO3 zPA1xTk1}ULMCDzqCn`-|0Zr@fzGi|s@C7LGslQt<0;oRE7Z*hZOV2nj0^)2zMh}!<#`;2iyBVuAocGx-VbHUG( zdCmmx{GD1*Uw^Bkv)(Gl6Yq5G(jX2iEIyY3Oa~2GfvtSn%J+NE32rC%`Ov%U8#}HQ zb9+s;N7;}Ae*Y1i$r?VGk}HetVPBSyfWoaxEiJqkRcof>52cLb*D5h4I^+Qx%M+2s zv;npflztVSn4uO*GHi&bldk(>SA$RgEls195QhD$uGN- zDX0lXXl8GaNq%wQ*PjG7nNT#E9YP3QCu0^r7{M|*ew?#dgh|5N*I@ib71hutCS4pW zt>P%{G3SaA7|#@=pLyJv*a>3d;$41!@S``c@C<1obUrtGhaPc<&SLNW`%POe2yTrt z>)Z&PSf zY$UP?b~3+X;8lyOuk^%*0Hpey+QS_(@RLai_VJO^FR#^7V}fc4`nV8wj7HDhz8$Ow zi(lHbY8-U{7SQ^Xpu|Z2;l^RD!;2n%SN6VZucZjei3<3ZRykuzTX;p(mT4$X{itVg zLrP%%)PchbDd#c}5+wlGXj;^Cn*ZTw8X`U<7qdj{H_jIm)^p;Q^hin>MMs6x5%bW! z`j@>Zv&#Itm|SW{a+QEy=`)Oa;Oa3r!B-DT!5^04OM4YSudY?NfCb!@CD4qWyrwRI zO&n1H<+N=2KoU>H6Y=)lF{Gta`SD6<5*CGE3Nqe{aAc%l8`zcPsqUeE=vcK`P8bMG zZxbkMg;-G5GyjsmdgE7gaNP*tjDm5G)h8j4NS&qXsaDuGS#Ggb0-tWuy8{&KU)w?e z|Khdd?DQ*q0^U85@7t{YdX2Gb04eD)hiSu`zl`=FU;T=#r8_&UAHfy$nVh}EA%1X{ zlYtukfj53&!ANJuM7Ho6$}cyIg_S@=42ic1S2}c;Nec~tbP>fFf8|WcaW;rfa*TJ& z=$&&MT;+kD;qe)3T*%OvBCcMwdh$_MSUtINe9e1*>{;TwV*?Ya+}pGVx7mn~y%cW1 z&r8^7g`@yVq=?=dr9TkDoRUKqq_$a`!w4)c=Ys)A9fki26OQ`$Vi|hvZYgS3(PQAy zz2sKk_@)e*7crQ-uBp5P? zHmwA$;WA}6{j|O!caHbI+_fpe9#&?#>$d56Fx-*IIzGZswk99||0Kkj35tA= zM(dx~4a6g6_k_~=w=ZzXhY`WCJJBbGSOwW^C$mj?5Wh#{H`J~><$$}4R_4~Nu(?O} z{SW6+Ws+$~t`D7)i zuML+YG%{FL^DWy0ki;%a_~hJa6m!Q@j?Zi=<+?_}nZfQCZ>hJ|NL|TjpA}{Yy$4H?&3fQ_ z(nNY<{S0b-0J&cQ1%?b$ZrO1cUIk^xk^hq3md3HcqM->|#(LV_y!KTSt)EckmaK%y2NywFiSydAg9usq5%nwk_&rSoX+J4RBFL)&z<-b1~xvgiF;?A#=#edo0p+i zIV;BBQ+_uK*4;MN)|@?KE>l%F&H%V;zb*Ib|EuUZ^0$WarY#5J7VN6dlFR$E0#v_p zIHoVF>iS38uRtAtB7L5mX%AZsQ@q4Qj5S0e2yi+|(>iOC1QHsNG zVv#;wPLx%q-hRqN_xHCw!;4brjqhD-4tL^ON0;5Vs0(2&*uwz(VzJ4U&z>;Evd1IJH# z%nViZC~pmo165#;ZzrrJGaAMgtkd>#om(1*54~(VT_nc<(~1FL%Z9grxPB@W6Eubj z!&%ipX1F7V3x^SJsOsKF-~h;zTyVk46lh>iPpMwfTz%2)7!|#1Q;<+C#P+@W zFbeEe7MOdC5M+Ra_VM>sObr%?`4`XYfYy*_HitckN_M%i>)W`?{XL`Z`}__vl~&xI zrkA(4>XRr{sY>kr`bXqw01S2mU|>f0A}pR`lF2!u?Fh|p_P!)7%Bi8h8#HcpO|ywb zRMp`Mr8Xh`50@wSIhfjA`$5fg2iU7$vI5FwoE>&PLWU=4GS#f-;wmQ51L!`JSc7a3 zRVJEM2_S9v@v`W6wT6{G_r;=za$S;a!3#)Ntn|>6yuF@VWwxoP$&c1xf@Db-zA&JHvt-yZeocL%5ek^GE zz{lY^abW{%fPcL3W};qY>>YnI(h<4GJccJi7?2Rc%^_)E%c6HP89$-8uwBLIdJVDKfa-?^6TH{r<$P+{8m0!+kgAuZA}r z1xfYh6-okJT;aOmGCYcd3F@@-or`-vNr8by{6CkxZnjKVT!x;(-1UNOGNj&2LaXdg z2m)x-3YIe_f}8<}REeAu8|y7d0fp>tS_hJlH`Ggc&Y`l{+J|{n6ILE~SToEl+-;=(S=!9^6M;L4bv}2l$1p74Vc#$jB;_D1WAS z8Ljdjnq-0@>&+MvmW0G}ZW}BY*KaXLfs!aPAj?OqJT&`CJz5E5F%*8W50g#25ga^x zuXqW3f(2kUi?SPb%J*)Ga1nY`wvEH;MRhs69zOeSTHW^PTE=upXyX5&f;DzoCR*8L z9bhxIAd=4`doC`ceyGLcfPfGPmThU8OKg&PyLK`Acd&drcqY2nd;wp-TN8$ac1dpX zb3Sx&F{DZk2;R)?AFaWUMNR7b9QVhZW{6-{UxVB7Jnb9O2PriOBDVu1QAd493RrZ* zn)rpu1kP1~>99p7InTag=;un3aa+S1{{Ikc7p1_CHar=K1As=tvQmj1I(fAPDRmxs zkB{?&vFGMNUcPN05ze1U1>e>-B5XJjQ53GDM)qmpILx8GzsaO&6MSM1Z^V6^*5DHw zkeA;W?!7jDCA{gpu!`?8me(GP<9_fkj_8Ilip2~p5q-*bsi(W!-(wxSmgK|ydY*MB z7v!!6xD7XxMIP|QQk&ETIpu>vKauxm2rAugPu4G9T()163<%?^Jq+fn?80=A_h!2+ z*Cq*K9MW2XFBwY5q6y1SA&bWX6jo+$^K*`|evNDge7UOp20Tb22P{N|@Jd~+O7I4z zpS1$V(iNGr94b1ARX;xbangPqp0l}2z9cbxk}}4nh92|U3bR>C9FRX8=uggK88+j3 z!BU(E+rJ7mCLzC!5~n&flz_v^V$7RoTM304M`h zkY7SZM|(emTWw$^hxW0uJz*?3$RJ*~L9`*Oo!@S-pisKsiGd z%W4~H^Y9NrAggmhR_DIMO33#jBG_*dyO`5;=)30og7338(}IV;q9+M-djt<(;w2E` zDOrApxYWDDXe1K3iVv8hFaQ`(RhfKy%*eM#dSJq?`<~r!8X)Dl1@;l=^low_PlO3~ zuPDW)CAa1%cQ&M$I;#t0XJM5J5N!jPg=sLmJZUNw;IK!Ym~!F3y3~p_QHk@2qY@Uq znDD>H#2o8PIi~L}F2y-G+gHqVm;eYh5eTameyLTRh5`ZWoqbkQQhBti>Q8DB$lMJay zEqR5Yy z+?v4FvPT{W??#}OE>wtZ6xI}qsCuOWf#Vxk%3Y8mv%>}s0lb<~&FpLCWkRgb-!9uY z6=+;C4j!Q=A%8tJeA3<~Iv0q%A_uQ~E>oh|x-YTdl`4@xp=OVXmp-$JCZnfu)*cZvsy}&6^;#53EHlrt{zA1tv`2@D+73RYY@MEn3^dC3Hw0#-QVo%u! z!R0X&Q-mGO9?t=wDn=QQ`N}iC;G66f&pEcSzK}8xZ+&@9Kmw3tKa7d%FsY9N2RVhG zh1eD4Z-PKMx@NE}r!dWxk@p?~RUEshmwd;!>^u@xL8X?s`wx>oef6E`}(-mW=y)#}^kpd_20bFsE| z5bW1WaB-O*Wha1exW{q;fXDY}Wb?po@PZz8ijEJjp%Q3pwh7vxZV?ZbJZnatTyYaf zzp&%1v+VBgZC5t1sn3~#vLY|u-aPH!m9jnB8XfOj3Q7eIq+;FpS`Wy|?LsQn+!!MT zy;0TId;|LOBjk3A*VeO>c*NPI=e^V{`xywnovCHcg^rU_N z+fPMc%o&wYR^>m&D%Hs^R6) zse)pz!_~Pmmur4urL{ROY}_7D**2?XhN?B6M%}a1Q($4#gwNUTIw1GEjX~JSRBYWT ze?7nHuE2Xbo zrZgB9Kdx|Y8CWM!)@MMPl%@S}?KZQ|i7S+1Yp^`Vl-@(jR=EBPiHeSD7)y_ApJRC5 z1=JHWP+BB9+W>(e9-+I6Y!6c0Q1WOv;bwHFAT@pk-RLLw^hVI>D_^V3$p6VIf zZc7QMcsBf48+1Wy@NTbZi31X6I80h9mz?JM5bz;Dp!Dp~q14+A$3Cv*x&|Y zLK=O_z-DO)3yphK*|t5d4Xs5SVgin$JTO!=(OvJY-0kY)Tg@a+z8&QC(cYZ&U|9CL!K7+n zjUoI|IG1+n5}E3j1R-NTM>MUm5()uwix-=!#wk6^-k5Ux!suEvF< zH1uNAv6m*xP^^0isV%^5f*fDoBFh+Q)8e{FQn~(s3+sboEUUER%{Q#<9pZaYdT;&K zI}+G|jkI(OsKp2?7xlr}aRNI4)9(`@0n`1mUc~~|5W_Fu9AWS2z6L z@}fA**|J0`hA1dXeWNsF>P zPh8T>4;rW@G&f@thM;9^=ch#h9cC=99F_4<)Bp*!sQ$VqrT#~U&9@5toRPH!%3e3Z z=x1uUetzjfQQaE;WbIQ|g?s2w(C#XFg(GxxueMuzTBG^cD_!VT%_7rjAiOd^oL%X? z5DfDjJ`Rj&f+<{+++B`VN`nD$7TdIFs<5?+%jMz2@sB$QEF8hBk4-usFl6Pnnjz`7 zZ^Tr=?CTopc&bF$n;{NUw;2kX?#CR8_G4`hqwNCs%rrMt)-jyBFMXZJ)?dy2y+gk> zTNcz62o^Z&Qd4n@u1+Cimp#O*fv+$~ERt(EadP&j-8!@NtHwKs8I-F6xdVn6w@zJm zOrt)9)W3(c+aLUwysA6NOUh?t0}D{Y(phr+Xv4o zuwSQLfWAr%*FA`NX@IYHDSWwl?Gdt;G0joOAM)hs&SQexow9_yF4JygnOv6FSaGf_ z;<_?CmrlZ$sewO%I%i)TJa-G|sKnLH*Kr}AhK=Vy_n_47VMZZ0qKH7?B>I_rwfiq4 z*tb3rCXntf`VN?0F4V@_5H^P}r`q=S+r)ULDA+z%pCLr)ue>*}JCS_reu{rt@gOhP zK#~$ErvLD$aqC^@fUImivio;G&I*h(Fy3a}d>a0O`o{8@)Et42$v|_0u{C=9Zb)qM zjZ-4O3kQ*C+sMbY6D8R)lU%tRZ#M4ZCfGS9OKQ|4l^4xyt4zx>7~AC9Gksg7-9&L- z0<-#4(%7Rx+9*=EJ=gtmSr##!VjlKW#C~KPecoXVV5IVkWcYhNs-FVv-k3sUAe8x2 z3^H6hRN;Dq@HiT@1Uuu5<#NLz(GlQ4bbD}HC*4SXN`tx&Y1v_uY0)rmj#&kTts_8t zx?ftH{U%%21(W=Vx`HTfSQ}gRS)4@HZvEVKOLD5qj4h&8fB#-$J*FeCn~uY|B-y5{ z5a3CCU+YJ^YI)AK1~FhrGFKYGtO8rhmxam5=!3m-NR0w5K_Cd#;T zyJy*PKEjg~x^ErGBAGzGtWyMD&|6itgL$g@bam*=8?%%HffGJivl&W}$#h_T*=T(+ z<@_|W{`}gJ`&rDxff@S0YV@C;m`GHcN@`sBe0cp7NpOvTjsGRfH*cVv(Joi>-PvR|5=*P1B?;tQ4VWZ^u z;d~NXBQ8Gs5s5LXn!L-qa7lrdljL-|;T5Ey*vqbXR+CY1ZF8w{?xLD?1%p8VK1>iy z8CC}>%NUq`I@bl)psG)fcQ^Nqge+3N9dW4H((a!i6Yi*>QOO)evWAb;t&AG)YFB}g zvIbR?12oVms{t=bg((xNR<&*Eq($qOqkLI_nS>ekg-M#oZw(sP2yp)Xt$R=p8}H5@ z3q3oWVtqejb)NbK4+OMg%Xhi(*GpPu`&UMxCU%7ERMWb8(84{`HDc5cM69f1J#y`V z(ba-{(oxq-4|7VNG?d_ZbZX0(f|$(ELcd`*7jAHYhJ7}%t)IS?$kBRdQb<%l=Ask(w1rGnmU>M)OlUA`W=a) zLtO@qD!r!{sQLD+yegraIu4%}Olz4(`*;39AgLeGwp1SZengSx)~-vjYydz?5xtSJ zr~Pc>3V2!X+H_qH*Hw{4`TMr3;eL-PIE9urw&`9|Oux(7-fmf5aH4c3(Wd9)w%9Mz zAZy|w_bp%)D`36MYqm(GcbTBUujsoPn5C#+@vomwIKC%I6;+^=kx2iQqPKj8UwvxOR1e7NtVpplwjtpgPPf?+7osji;kr3a zU1=0ozvz}x?;P&!y4dd1O5X)r|FH5?R>ewX5$Hg6KB2XZKe;BUl`QXWzv!CWeUjx* zrCk!UA2XXvrEQxYFk?9FXI?b}z_46=&uFqIu+cZc%1pp8%MBxX+$zLtNCCc&+WOu$ zhLT(uBG6&7c~V}pQ)Yx~Q#PM@(7^0KF+1)lEeZm9Xw0%+5! zjT^s+0CN4xOMu;1OHVnaT&52kg%o4T8B1#08I7mTVauip8t2OyY)3uXmw%rN;HvMI z9}*ic!=~|ZL{zIY*IR(yxfVjZDA{O55tsySD7){qwHWkaPuXHDO_GWWgFTzlWp7gL^J=XGM^UUq~ZTyD@DMhaay_; zV%gUgHgPfdY5L7a$jvaK`;Cn0&&4jpUmW029jV{=uC~OYn6lI~PO9XW??{|DEt-1n z&Ot}1f*X;|X!{D?ADBb#?g{mk@FYi#fN5Xps8cWFJyqUoK;%d*P?L^pJ;_0R{-TfNk0S{sR68lg6ophj=Tb3(wJcq9((53vpuLT%`Za(uMP)}{1yXOgU&5g3K)+Sm!z%-*ImidM@h7|6`^&j!7nJ9cV^UMS*Uv2j2EeWWBk&+9!*!$DDC>m=6qKaQq=dgm02ePe2E@?3I0;a|GHE zac=epE+jJwY=5#r9 zafKv|dC`Nn_}$_3^K->(DQd~0yBmPvANqiBHq2Xc%wrS z7D_Q0m+u7%8(Co1HVPk8>pKoqIY(5lG{Y>=Ow3*ty3O0AEc*Jye%B9C1^Y7~JcyRG z)WQ05-bn>Z8EECmnR;4}Oi<)mZ@o~U_fz&+YDX})VCAUI@!ncw=wgeBF0x+3e;hb^ z+wH1hCwq+aSyl#pFXhhxyAANQlqkZ;>i%yUXLBW4)*W8yTCV$pbk zy)4El84gu~za3YYdQ1(~u%rgKk2Dc{7D&Eap|`0|STqdUsA}!8%VS<)nw)$1wf8jH!F*qr*-D_HN>94juh#6LZD>dIv(5 zn=u+0zhm$=O@4biDFL#FT+&}p@J(}II?gecjoE!H4Nl@0KC7bzp&z056szw+3elm_ zcM4@`fJB&GAm8;BZA+GRbXGTWz?8Xv?5z{s+F{D=bY8T5Yzf}2FRTCIFBGIfcq&o>@|e`q zZx8*%Dci3xh3=ct;3P%V2$Q9srMlbLZ}uf=S+%*8Oc$P$J-JG_KD+%vFe@3Dmt6+8 z=5y)a3xd(`+j!Yp03!lFf7S`eu*%8Td*<74HW@fxBmHPmXJ7&SQR=vmJ_{Xa*FEv% zJ{kbH^V>RBnvM3>17^Lk=)S<3OSpaAC%N^K@2%QHw=ZVvm@LEU^k$C1NDUQNrM24C zA#nPm1Ll2E&}gq!M%*ls%JucTc-ik`Y5-%2fmq^gm~eEbGcO`Or6@2`frETB>TvZL zY_fB_vVO)hN%v^G!7?AykFW`lV1IB|60$2Yf?WaeUbgqt=dgVs`vS^Pri{I-v_+?n zk*v#uPHEakL%;H&dhT+ZiKF;wMF?qopR5XEE&)5OvDwxrY(XiYpJK4>F`FUQZGE4%SCJ>-3|ulQVcgC8B+roH=%MaPyFr1w#ABJ zyN2QXNSB6VdJ=qndyYo((D+UwKQYcho8@6lb(-N<`wVfnldg>p>K4p1&3d@=)Rp@s zpHTN}d5*g9dh&BZ5X7#4lgsOIue_xZ@es>aD~u*Qn)*4TvD&Krg#EPerq$L=LR;PG z4YAZPEsYRoX1IECQ&rhhr8kH2#~H$+t|rIdZyHDh1M z;dDxJh**VTZDwqcuimZ>!T%U~lh&s-PO3%L3mDoFX7}9Roa?EZ&b<*lGby^l0^|Y% zVc~KtHmUI|VqE>qATB5ZjqH=YnWPGhR0yr;_cz~hu~V2Dl!>gMaX7=gH!P0{L378dv!BZZ1*lcLBrZzmBVlLX2y6qKgpu6agT+ziI7HfejTSbIyfE*Z=F z2+@1m@@b*E{?+u>+$yXeAnz%zb!sfDSrJ|2mGS&#BFQ#msk`h5bB1JE=X~zH>DEWH zR@jtS&Am)8m)OrGUxMGXl+{|+Id{sw)l=_cm*yLp$o(44P}~!$A9Q>=S_gOd!Pfh0 zqi)6Tl9hf!%dUQoqgyM$6K-(UZsUX>llenEJW!Z|g^D8oLi5mi4TWDNq+R2yi-Meq zH*S*IhvRfh*Info!l!eQcmX1Tdg+vxzBlM#>iNSC(r%{B7{7wmkrqYMInK-WgteG1 z_at5MPXB&Y(%2}f6Y=J9(aZXs*M=M3__cMUevLWXB{MT{P;6`8ffHy-vdi(U^}ZkD z(aPlbsx5#_uvA2doXTqq!`lKYV4W9w#Vw<`n)LLCDoIB#55_LPziXdwK>*a)jP7N0 z=AbUb*h4iy)K`x>{gF;xVnzIAg1S6yJx=>yvDJ8b-=Exd+noCC7iiqpojoOybJ8V&?YXAc#j?jp-Hf{VF7_H{uXVd>G#9 z?86f0a0GtWF&AFMLjMj=QtaE4Q11?z^!k~O?RW4(GgrN2_j1pn%{54O+Mv3Z)z8!! z;@Qqk>mR{Tgzv|Nb=aiG2zy{z-T{d|Hcq8jg^gK75C~dB0BRv5aR#cLVB4+?c{SJ@_-C?Sm;o<2j7Y z;}}6xFxA=b_qn~pAkWay%_Z#Qvx!hG$KEqsYaYNi?EIk9R z@z+n6=G}?zHk)ge**|02R2U4mwIs*l-?WvJzPfI;rYYA zBBv`2T@fDG&eQq*9WrS4&CJNQ_S9ws(<@~VF-rLbB=G2dNe}hIfEqGJ6C4$aAH{)@ zE?4&K7N^23->gLE!1<|(n{jS#2_k7B)Q$^v)-L)SmAoPQmw{BhIQ$_;D6W1pl1H$r zBy;>O+DG39%vGydu>C5@QP8p?QJHUNd-M(U`|ZB{Esh|Jj3(~!1^oU+tABEB)mvb$o5|)K zX)Ngpf@;?9^tT&+>#61wG{!sn`nUpwKe<#B$D3{X^u+NILb0lTzj$R_C78rg=F$u{ zSK=7o)L;SX*H1>Da;a_Xu6{Kt$7PznOsE$+1RvY@qP6nAMtFLa74%adY6vNeSKC~f zf`NmHv1eT|v<~Cu7TL9unsj*5j??!prGtkk99vkbqv-p`8VR2*Ftis~bL+H>UNcS) zQPjCjITo_x9i*Kk`KIWMf`Suv*QN&ku4PAcd4a-v@ps^spkAho{PXf#EBf}xbJ8z% zP#2SBsenNys06@KW|DhX6;LfM3OL;_IB-}th3kFw9Fq4Gofgq?*$y9G}8K~{+y7V|r=tale=*4^p|+AbZF>TNsa zx0A&^@Hl-5nxI=Ql`Nxs39prHIP$j0?{iSeK>0q<3{tXg{IC-Gq2z8@#05Ug}4tsXpl}C%U2Q8iBuVQb1}WN2|Hv1$2ot-+`eE%;+|5HM)XPRyvqKu zUO%gMIc!K!OZC;3ajwJs>C(}uv(#z-!;uWmj6M5vhtYXYTOF?I5d^iEmv{(_FLV&@!noN+<$5wCMq1`hJuGzi+6hfb zrl)dnj=j@i_J}^Og61vnh?#D1R(4n>;j@rRTra;7apPo2W zeWX17%uCS~3}J1Bg>p$=zvEb@E5)$;S1;B&Cy$)$H$F_uokb$SmL9N$<7W{VE|8I zoq$lm;blOVRRaryQs6a#2MR(D^9V1y6ycAk|3HdKhF#$K4-0nC$ra8mEqjNNUv~XP z=9^(|`z}pEvQE^|8C@;mF@(-;eVG%?}j|=p~i@+ z?L~F|xe|Bw=1J-C*SS3Xfx7))@!*LZ3!g?0p;ovO7cqS64$G=&6L(g>oUR$d`hM=s zl2|g=Ut(ubY_wgc~sT7#YE z@hSrE_zz&A947t^*2cTW1%7-kX12o!j$j0K+2BiU&h!NQ1aiU?&s}>Cai1W8*fyQ( zmGzS=un9S1H}^MzP3s{JgWr z5D>CTASax%yubkM6)dtz22y+jKaOh8J$L0|JR|Df3J1@ zsQiZ1*FV1h|9Y8$F}OeD!q31W_V2a++h6fw$o6{O4WZF(dXuZrtZ) z{O4VN7w7Nd{EsvHZ{++WW8>%aNE z|39#T95hZ_YYR`f4+x415bw^_O++i!bc!k7Bzh6 tFF+dooX67g|MK=bh;deh;cG-f#Mzs9^A4Ek0`Fa8@O1TaS?83{1OPwr*F^vT