@@ -102,64 +102,72 @@ Below is the implementation of the solution of the 2-SAT problem for the already
102102In the graph the vertices with indices $2k$ and $2k+1$ are the two vertices corresponding to variable $k$ with $2k+1$ corresponding to the negated variable.
103103
104104``` {.cpp file=2sat}
105- int n;
106- vector<vector<int >> adj, adj_t ;
107- vector<bool > used;
108- vector<int > order, comp;
109- vector<bool > assignment;
110-
111- void dfs1 (int v) {
112- used[ v] = true;
113- for (int u : adj[ v] ) {
114- if (!used[ u] )
115- dfs1(u);
105+ struct TwoSatSolver {
106+ int n;
107+ vector<vector<int >> adj, adj_t;
108+ vector<bool > used;
109+ vector<int > order, comp;
110+ vector<bool > assignment;
111+
112+ // n is the number of variables
113+ TwoSatSolver(int n) : n(n), adj(2 * n), adj_t(2 * n), used(2 * n), order(), comp(2 * n, -1), assignment(n) {
114+ order.reserve(2 * n);
116115 }
117- order.push_back(v);
118- }
119-
120- void dfs2 (int v, int cl ) {
121- comp [ v ] = cl;
122- for (int u : adj_t [ v ] ) {
123- if (comp [ u ] == -1)
124- dfs2(u, cl );
116+
117+ void dfs1 (int v) {
118+ used [ v ] = true;
119+ for (int u : adj [ v ] ) {
120+ if (!used [ u ] )
121+ dfs1(u);
122+ }
123+ order.push_back(v );
125124 }
126- }
127-
128- bool solve_2SAT() {
129- order.clear();
130- used.assign(n, false);
131- for (int i = 0; i < n; ++i) {
132- if (!used[ i] )
133- dfs1(i);
125+
126+ void dfs2(int v, int cl) {
127+ comp[v] = cl;
128+ for (int u : adj_t[v]) {
129+ if (comp[u] == -1)
130+ dfs2(u, cl);
131+ }
134132 }
135133
136- comp.assign(n, -1);
137- for (int i = 0, j = 0; i < n; ++i) {
138- int v = order[n - i - 1];
139- if (comp[v] == -1)
140- dfs2(v, j++);
134+ // m will be the number of vertices in the graph (= 2 * n)
135+ bool solve_2SAT(int m) {
136+ order.clear();
137+ used.assign(m, false);
138+ for (int i = 0; i < m; ++i) {
139+ if (!used[i])
140+ dfs1(i);
141+ }
142+
143+ comp.assign(m, -1);
144+ for (int i = 0, j = 0; i < m; ++i) {
145+ int v = order[m - i - 1];
146+ if (comp[v] == -1)
147+ dfs2(v, j++);
148+ }
149+
150+ assignment.assign(m / 2, false);
151+ for (int i = 0; i < m; i += 2) {
152+ if (comp[i] == comp[i + 1])
153+ return false;
154+ assignment[i / 2] = comp[i] > comp[i + 1];
155+ }
156+ return true;
141157 }
142158
143- assignment.assign(n / 2, false);
144- for (int i = 0; i < n; i += 2) {
145- if (comp[i] == comp[i + 1])
146- return false;
147- assignment[i / 2] = comp[i] > comp[i + 1];
159+ void add_disjunction(int a, bool na, int b, bool nb) {
160+ // na and nb signify whether a and b are to be negated
161+ a = 2 * a ^ na;
162+ b = 2 * b ^ nb;
163+ int neg_a = a ^ 1;
164+ int neg_b = b ^ 1;
165+ adj[neg_a].push_back(b);
166+ adj[neg_b].push_back(a);
167+ adj_t[b].push_back(neg_a);
168+ adj_t[a].push_back(neg_b);
148169 }
149- return true;
150- }
151-
152- void add_disjunction(int a, bool na, int b, bool nb) {
153- // na and nb signify whether a and b are to be negated
154- a = 2* a ^ na;
155- b = 2* b ^ nb;
156- int neg_a = a ^ 1;
157- int neg_b = b ^ 1;
158- adj[ neg_a] .push_back(b);
159- adj[ neg_b] .push_back(a);
160- adj_t[ b] .push_back(neg_a);
161- adj_t[ a] .push_back(neg_b);
162- }
170+ };
163171```
164172
165173## Practice Problems
0 commit comments