2-SAT, which stands for 2-Satisfiability, is a logical problem.
The key point is that you are given a logical expression with variables, and you must assign 0s and 1s to the variables such that all conditions are satisfied, or declare that it's impossible. This expression resembles something like \(({a_1} ∨ {b_1}) ∧ ({a_2} ∨ {b_2}) ∧ ··· ∧ ({a_m} ∨ {b_m})\), where \(a_i\) and \(b_i\) are either variables from \(({x_1}, {x_2},..., {x_n})\) or their negations, i.e., \(({¬x_1}, {¬x_2},..., {¬x_n})\).
1int n;
2cin >> n;
3// here we check a
4if (a) {
5 // if it was valid
6 cout << "YES" << endl;
7}
Initially, for each variable and its negation, we create a vertex in the graph (totaling 2n vertices). For each clause \(u ∨ w\), we add a directed edge from the negation of u to w, and a directed edge from the negation of w to u.
If two vertices u and its negation are in the same strongly connected component (SCC), it means the clause cannot be satisfied. This is because if u is assigned 1, its negation must also be 1, and if u is 0, its negation must also be 0—leading to a contradiction.
Using Kosaraju's algorithm, we can determine whether any vertex and its negation reside in the same SCC.
If the above condition is not met (i.e., no variable shares an SCC with its negation), the formula can be satisfied. We then proceed to assign values to the variables.
We perform a topological sort on the vertices of the graph. If a vertex u appears after its negation in the topological order, we assign it 1; if it appears before its negation, we assign it 0.
This algorithm has a time complexity of \(O(n + m)\).
One of the applications of 2-SAT is detecting bipartiteness of graphs. For each vertex, we consider a variable. If two vertices u and v are connected by an edge, we add two conditions \((a_v ∨ ¬a_u) ∧ (¬a_v ∨ a_u)\) to the 2-SAT formula.
Clearly, this approach allows us to detect bipartite graphs. By assigning one partition as 0 and the other as 1, the 2-SAT conditions are satisfied. Therefore, if a solution exists, it means the graph is bipartite.
A more difficult problem than 2-SAT, where each clause contains three variables instead of two. This problem is NP-complete and therefore has no efficient known algorithm. It is stated that all K-SAT problems (where k > 3) can be converted to 3-SAT.