From b67bcc5b6200dc43fa24c46e05e1ab77333166ae Mon Sep 17 00:00:00 2001 From: Kevin Sheng Date: Mon, 1 Jul 2024 02:57:01 -0700 Subject: [PATCH 1/2] better 2sat impl --- content/6_Advanced/SCC.mdx | 145 ++++++++++++++++++++----------------- 1 file changed, 77 insertions(+), 68 deletions(-) diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index 2c9fdd1949..b77fb1edc3 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -227,8 +227,8 @@ class TarjanSolver { const vector> &adj; TarjanSolver(const vector> &adj) - : adj(adj), rev_adj(adj.size()), post(adj.size()), comp(adj.size()), - visited(adj.size()) { + : 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; @@ -239,7 +239,7 @@ class TarjanSolver { if (!visited[n]) { fill_post(n); } } std::sort(nodes.begin(), nodes.end(), - [&](int n1, int n2) { return post[n1] > post[n2]; }); + [&](int n1, int n2) { return post[n1] > post[n2]; }); visited.assign(adj.size(), false); for (int n : nodes) { @@ -361,7 +361,7 @@ using std::vector; // BeginCodeSnip{SCC Solver} class TarjanSolver { - private: + private: vector> rev_adj; vector post; vector comp; @@ -373,7 +373,9 @@ class TarjanSolver { void fill_post(int at) { visited[at] = true; for (int n : rev_adj[at]) { - if (!visited[n]) { fill_post(n); } + if (!visited[n]) { + fill_post(n); + } } post[at] = timer++; } @@ -382,26 +384,35 @@ class TarjanSolver { visited[at] = true; comp[at] = id; for (int n : adj[at]) { - if (!visited[n]) { find_comp(n); } + 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()) { + 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 next : adj[n]) { + rev_adj[next].push_back(n); + } } for (int n = 0; n < adj.size(); n++) { - if (!visited[n]) { fill_post(n); } + if (!visited[n]) { + fill_post(n); + } } std::sort(nodes.begin(), nodes.end(), - [&](int n1, int n2) { return post[n1] > post[n2]; }); + [&](int n1, int n2) { return post[n1] > post[n2]; }); visited.assign(adj.size(), false); for (int n : nodes) { @@ -419,75 +430,74 @@ class TarjanSolver { // EndCodeSnip struct Clause { - int var1; // id of the first variable + 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; } +/** + * @return a vector of booleans that satisfy the given clauses, + * or an empty vector if no such set of booleans exist + */ +vector solve_sat(const vector& clauses, int var_num) { + vector> adj(2 * var_num); + // 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); + } - 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)) { + return {}; } + comps[scc.get_comp(i)].push_back(i); + comps[scc.get_comp(i + 1)].push_back(i + 1); + } - 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; + vector val(2 * var_num, -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) { + int neg = v % 2 == 1 ? v - 1 : v + 1; + if (val[neg] != -1) { + set_to = !val[neg]; + break; } - 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; } + for (int v : comp) { + val[v] = set_to; } } - - bool is_valid() const { return valid; } - - bool get_var(int var) const { return val[2 * var]; } -}; + + vector actual_val(var_num); + for (int i = 0; i < var_num; i++) { + actual_val[i] = val[2 * i]; + } + + return actual_val; +} int main() { int req_num; int topping_num; std::cin >> req_num >> topping_num; vector clauses(req_num); - for (Clause &c : clauses) { + for (Clause& c : clauses) { char neg1, neg2; std::cin >> neg1 >> c.var1 >> neg2 >> c.var2; c.var1--; @@ -496,14 +506,13 @@ int main() { c.neg2 = neg2 == '-'; } - SATSolver sat(clauses, topping_num); - if (!sat.is_valid()) { + vector sat_res = solve_sat(clauses, topping_num); + if (sat_res.empty()) { cout << "IMPOSSIBLE" << endl; } else { for (int t = 0; t < topping_num; t++) { - cout << (sat.get_var(t) ? '+' : '-') << ' '; + cout << (sat_res[t] ? '+' : '-') << " \n"[t == topping_num - 1]; } - cout << endl; } } ``` From 1030212a04d39073f6c65842fccb4bbc9d461e22 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Mon, 1 Jul 2024 09:59:42 +0000 Subject: [PATCH 2/2] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- content/6_Advanced/SCC.mdx | 65 ++++++++++++++------------------------ 1 file changed, 24 insertions(+), 41 deletions(-) diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index b77fb1edc3..acfa4eb28d 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -227,8 +227,8 @@ class TarjanSolver { const vector> &adj; TarjanSolver(const vector> &adj) - : adj(adj), rev_adj(adj.size()), post(adj.size()), comp(adj.size()), - visited(adj.size()) { + : 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; @@ -239,7 +239,7 @@ class TarjanSolver { if (!visited[n]) { fill_post(n); } } std::sort(nodes.begin(), nodes.end(), - [&](int n1, int n2) { return post[n1] > post[n2]; }); + [&](int n1, int n2) { return post[n1] > post[n2]; }); visited.assign(adj.size(), false); for (int n : nodes) { @@ -361,7 +361,7 @@ using std::vector; // BeginCodeSnip{SCC Solver} class TarjanSolver { - private: + private: vector> rev_adj; vector post; vector comp; @@ -373,9 +373,7 @@ class TarjanSolver { void fill_post(int at) { visited[at] = true; for (int n : rev_adj[at]) { - if (!visited[n]) { - fill_post(n); - } + if (!visited[n]) { fill_post(n); } } post[at] = timer++; } @@ -384,35 +382,26 @@ class TarjanSolver { visited[at] = true; comp[at] = id; for (int n : adj[at]) { - if (!visited[n]) { - find_comp(n); - } + 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()) { + 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 next : adj[n]) { rev_adj[next].push_back(n); } } for (int n = 0; n < adj.size(); n++) { - if (!visited[n]) { - fill_post(n); - } + if (!visited[n]) { fill_post(n); } } std::sort(nodes.begin(), nodes.end(), - [&](int n1, int n2) { return post[n1] > post[n2]; }); + [&](int n1, int n2) { return post[n1] > post[n2]; }); visited.assign(adj.size(), false); for (int n : nodes) { @@ -430,7 +419,7 @@ class TarjanSolver { // EndCodeSnip struct Clause { - int var1; // id of the first variable + int var1; // id of the first variable bool neg1; // is it negated? int var2; bool neg2; @@ -440,10 +429,10 @@ struct Clause { * @return a vector of booleans that satisfy the given clauses, * or an empty vector if no such set of booleans exist */ -vector solve_sat(const vector& clauses, int var_num) { +vector solve_sat(const vector &clauses, int var_num) { vector> adj(2 * var_num); // 2 * var is the variable, while 2 * var + 1 is its negation - for (const Clause& c : clauses) { + 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 @@ -455,9 +444,7 @@ vector solve_sat(const vector& clauses, int var_num) { 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)) { - return {}; - } + if (scc.get_comp(i) == scc.get_comp(i + 1)) { return {}; } comps[scc.get_comp(i)].push_back(i); comps[scc.get_comp(i + 1)].push_back(i + 1); } @@ -468,7 +455,7 @@ vector solve_sat(const vector& clauses, int var_num) { * starting from comp 0 and going up process the graph * in reverse topological order- neat, huh? */ - for (const vector& comp : comps) { + 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) { @@ -479,16 +466,12 @@ vector solve_sat(const vector& clauses, int var_num) { } } - for (int v : comp) { - val[v] = set_to; - } + for (int v : comp) { val[v] = set_to; } } - + vector actual_val(var_num); - for (int i = 0; i < var_num; i++) { - actual_val[i] = val[2 * i]; - } - + for (int i = 0; i < var_num; i++) { actual_val[i] = val[2 * i]; } + return actual_val; } @@ -497,7 +480,7 @@ int main() { int topping_num; std::cin >> req_num >> topping_num; vector clauses(req_num); - for (Clause& c : clauses) { + for (Clause &c : clauses) { char neg1, neg2; std::cin >> neg1 >> c.var1 >> neg2 >> c.var2; c.var1--;