diff --git a/content/6_Advanced/SCC.mdx b/content/6_Advanced/SCC.mdx index 2c9fdd1949..acfa4eb28d 100644 --- a/content/6_Advanced/SCC.mdx +++ b/content/6_Advanced/SCC.mdx @@ -425,62 +425,55 @@ struct Clause { 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; } + vector actual_val(var_num); + for (int i = 0; i < var_num; i++) { actual_val[i] = val[2 * i]; } - bool get_var(int var) const { return val[2 * var]; } -}; + return actual_val; +} int main() { int req_num; @@ -496,14 +489,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; } } ```