|
| 1 | +package com.thealgorithms.datastructures.graphs; |
| 2 | + |
| 3 | +import java.util.ArrayList; |
| 4 | +import java.util.Arrays; |
| 5 | +import java.util.Stack; |
| 6 | + |
| 7 | +/** |
| 8 | + * This class implements a solution to the 2-SAT (2-Satisfiability) problem |
| 9 | + * using Kosaraju's algorithm to find strongly connected components (SCCs) |
| 10 | + * in the implication graph. |
| 11 | + * |
| 12 | + * <p> |
| 13 | + * <strong>Brief Idea:</strong> |
| 14 | + * </p> |
| 15 | + * |
| 16 | + * <pre> |
| 17 | + * 1. From each clause (a ∨ b), we can derive implications: |
| 18 | + * (¬a → b) and (¬b → a) |
| 19 | + * |
| 20 | + * 2. We construct an implication graph using these implications. |
| 21 | + * |
| 22 | + * 3. For each variable x, its negation ¬x is also represented as a node. |
| 23 | + * If x and ¬x belong to the same SCC, the expression is unsatisfiable. |
| 24 | + * |
| 25 | + * 4. Otherwise, we assign truth values based on the SCC order: |
| 26 | + * If SCC(x) > SCC(¬x), then x = true; otherwise, x = false. |
| 27 | + * </pre> |
| 28 | + * |
| 29 | + * <p> |
| 30 | + * <strong>Complexities:</strong> |
| 31 | + * </p> |
| 32 | + * <ul> |
| 33 | + * <li>Time Complexity: O(n + m)</li> |
| 34 | + * <li>Space Complexity: O(n + m)</li> |
| 35 | + * </ul> |
| 36 | + * where {@code n} is the number of variables and {@code m} is the number of |
| 37 | + * clauses. |
| 38 | + * |
| 39 | + * <p> |
| 40 | + * <strong>Usage Example:</strong> |
| 41 | + * </p> |
| 42 | + * |
| 43 | + * <pre> |
| 44 | + * TwoSat twoSat = new TwoSat(5); // Initialize with 5 variables: x1, x2, x3, x4, x5 |
| 45 | + * |
| 46 | + * // Add clauses |
| 47 | + * twoSat.addClause(1, false, 2, false); // (x1 ∨ x2) |
| 48 | + * twoSat.addClause(3, true, 2, false); // (¬x3 ∨ x2) |
| 49 | + * twoSat.addClause(4, false, 5, true); // (x4 ∨ ¬x5) |
| 50 | + * |
| 51 | + * twoSat.solve(); // Solve the problem |
| 52 | + * |
| 53 | + * if (twoSat.isSolutionExists()) { |
| 54 | + * boolean[] solution = twoSat.getSolutions(); |
| 55 | + * for (int i = 1; i <= 5; i++) { |
| 56 | + * System.out.println("x" + i + " = " + solution[i]); |
| 57 | + * } |
| 58 | + * } |
| 59 | + * </pre> |
| 60 | + * <p><strong>Reference</strong></p> |
| 61 | + * <a href="https://cp-algorithms.com/graph/2SAT.html">CP Algorithm</a> <br></br> |
| 62 | + * <a href="https://en.wikipedia.org/wiki/2-satisfiability">Wikipedia - 2 SAT</a> |
| 63 | + * @author Shoyeb Ansari |
| 64 | + * |
| 65 | + * @see Kosaraju |
| 66 | + */ |
| 67 | +class TwoSat { |
| 68 | + |
| 69 | + /** Number of variables in the boolean expression. */ |
| 70 | + private final int numberOfVariables; |
| 71 | + |
| 72 | + /** Implication graph built from the boolean clauses. */ |
| 73 | + private final ArrayList<Integer>[] graph; |
| 74 | + |
| 75 | + /** Transposed implication graph used in Kosaraju's algorithm. */ |
| 76 | + private final ArrayList<Integer>[] graphTranspose; |
| 77 | + |
| 78 | + /** Stores one valid truth assignment for all variables (1-indexed). */ |
| 79 | + private final boolean[] variableAssignments; |
| 80 | + |
| 81 | + /** Indicates whether a valid solution exists. */ |
| 82 | + private boolean hasSolution = true; |
| 83 | + |
| 84 | + /** Tracks whether the {@code solve()} method has been called. */ |
| 85 | + private boolean isSolved = false; |
| 86 | + |
| 87 | + /** |
| 88 | + * Initializes the TwoSat solver with the given number of variables. |
| 89 | + * |
| 90 | + * @param numberOfVariables the number of boolean variables |
| 91 | + * @throws IllegalArgumentException if the number of variables is negative |
| 92 | + */ |
| 93 | + @SuppressWarnings({"unchecked", "rawtypes"}) |
| 94 | + TwoSat(int numberOfVariables) { |
| 95 | + if (numberOfVariables < 0) { |
| 96 | + throw new IllegalArgumentException("Number of variables cannot be negative."); |
| 97 | + } |
| 98 | + this.numberOfVariables = numberOfVariables; |
| 99 | + int n = 2 * numberOfVariables + 1; |
| 100 | + |
| 101 | + graph = (ArrayList<Integer>[]) new ArrayList[n]; |
| 102 | + graphTranspose = (ArrayList<Integer>[]) new ArrayList[n]; |
| 103 | + for (int i = 0; i < n; i++) { |
| 104 | + graph[i] = new ArrayList<>(); |
| 105 | + graphTranspose[i] = new ArrayList<>(); |
| 106 | + } |
| 107 | + variableAssignments = new boolean[numberOfVariables + 1]; |
| 108 | + } |
| 109 | + |
| 110 | + /** |
| 111 | + * Adds a clause of the form (a ∨ b) to the boolean expression. |
| 112 | + * |
| 113 | + * <p> |
| 114 | + * Example: To add (¬x₁ ∨ x₂), call: |
| 115 | + * </p> |
| 116 | + * |
| 117 | + * <pre>{@code |
| 118 | + * addClause(1, true, 2, false); |
| 119 | + * }</pre> |
| 120 | + * |
| 121 | + * @param a the first variable (1 ≤ a ≤ numberOfVariables) |
| 122 | + * @param isNegateA {@code true} if variable {@code a} is negated |
| 123 | + * @param b the second variable (1 ≤ b ≤ numberOfVariables) |
| 124 | + * @param isNegateB {@code true} if variable {@code b} is negated |
| 125 | + * @throws IllegalArgumentException if {@code a} or {@code b} are out of range |
| 126 | + */ |
| 127 | + void addClause(int a, boolean isNegateA, int b, boolean isNegateB) { |
| 128 | + if (a <= 0 || a > numberOfVariables) { |
| 129 | + throw new IllegalArgumentException("Variable number must be between 1 and " + numberOfVariables); |
| 130 | + } |
| 131 | + if (b <= 0 || b > numberOfVariables) { |
| 132 | + throw new IllegalArgumentException("Variable number must be between 1 and " + numberOfVariables); |
| 133 | + } |
| 134 | + |
| 135 | + a = isNegateA ? negate(a) : a; |
| 136 | + b = isNegateB ? negate(b) : b; |
| 137 | + int notA = negate(a); |
| 138 | + int notB = negate(b); |
| 139 | + |
| 140 | + // Add implications: (¬a → b) and (¬b → a) |
| 141 | + graph[notA].add(b); |
| 142 | + graph[notB].add(a); |
| 143 | + |
| 144 | + // Build transpose graph |
| 145 | + graphTranspose[b].add(notA); |
| 146 | + graphTranspose[a].add(notB); |
| 147 | + } |
| 148 | + |
| 149 | + /** |
| 150 | + * Solves the 2-SAT problem using Kosaraju's algorithm to find SCCs |
| 151 | + * and determines whether a satisfying assignment exists. |
| 152 | + */ |
| 153 | + void solve() { |
| 154 | + isSolved = true; |
| 155 | + int n = 2 * numberOfVariables + 1; |
| 156 | + |
| 157 | + boolean[] visited = new boolean[n]; |
| 158 | + int[] component = new int[n]; |
| 159 | + Stack<Integer> topologicalOrder = new Stack<>(); |
| 160 | + |
| 161 | + // Step 1: Perform DFS to get topological order |
| 162 | + for (int i = 1; i < n; i++) { |
| 163 | + if (!visited[i]) { |
| 164 | + dfsForTopologicalOrder(i, visited, topologicalOrder); |
| 165 | + } |
| 166 | + } |
| 167 | + |
| 168 | + Arrays.fill(visited, false); |
| 169 | + int sccId = 0; |
| 170 | + |
| 171 | + // Step 2: Find SCCs on transposed graph |
| 172 | + while (!topologicalOrder.isEmpty()) { |
| 173 | + int node = topologicalOrder.pop(); |
| 174 | + if (!visited[node]) { |
| 175 | + dfsForScc(node, visited, component, sccId); |
| 176 | + sccId++; |
| 177 | + } |
| 178 | + } |
| 179 | + |
| 180 | + // Step 3: Check for contradictions and assign values |
| 181 | + for (int i = 1; i <= numberOfVariables; i++) { |
| 182 | + int notI = negate(i); |
| 183 | + if (component[i] == component[notI]) { |
| 184 | + hasSolution = false; |
| 185 | + return; |
| 186 | + } |
| 187 | + // If SCC(i) > SCC(¬i), then variable i is true. |
| 188 | + variableAssignments[i] = component[i] > component[notI]; |
| 189 | + } |
| 190 | + } |
| 191 | + |
| 192 | + /** |
| 193 | + * Returns whether the given boolean formula is satisfiable. |
| 194 | + * |
| 195 | + * @return {@code true} if a solution exists; {@code false} otherwise |
| 196 | + * @throws Error if called before {@link #solve()} |
| 197 | + */ |
| 198 | + boolean isSolutionExists() { |
| 199 | + if (!isSolved) { |
| 200 | + throw new Error("Please call solve() before checking for a solution."); |
| 201 | + } |
| 202 | + return hasSolution; |
| 203 | + } |
| 204 | + |
| 205 | + /** |
| 206 | + * Returns one valid assignment of variables that satisfies the boolean formula. |
| 207 | + * |
| 208 | + * @return a boolean array where {@code result[i]} represents the truth value of |
| 209 | + * variable {@code xᵢ} |
| 210 | + * @throws Error if called before {@link #solve()} or if no solution exists |
| 211 | + */ |
| 212 | + boolean[] getSolutions() { |
| 213 | + if (!isSolved) { |
| 214 | + throw new Error("Please call solve() before fetching the solution."); |
| 215 | + } |
| 216 | + if (!hasSolution) { |
| 217 | + throw new Error("No satisfying assignment exists for the given expression."); |
| 218 | + } |
| 219 | + return variableAssignments.clone(); |
| 220 | + } |
| 221 | + |
| 222 | + /** Performs DFS to compute topological order. */ |
| 223 | + private void dfsForTopologicalOrder(int u, boolean[] visited, Stack<Integer> topologicalOrder) { |
| 224 | + visited[u] = true; |
| 225 | + for (int v : graph[u]) { |
| 226 | + if (!visited[v]) { |
| 227 | + dfsForTopologicalOrder(v, visited, topologicalOrder); |
| 228 | + } |
| 229 | + } |
| 230 | + topologicalOrder.push(u); |
| 231 | + } |
| 232 | + |
| 233 | + /** Performs DFS on the transposed graph to identify SCCs. */ |
| 234 | + private void dfsForScc(int u, boolean[] visited, int[] component, int sccId) { |
| 235 | + visited[u] = true; |
| 236 | + component[u] = sccId; |
| 237 | + for (int v : graphTranspose[u]) { |
| 238 | + if (!visited[v]) { |
| 239 | + dfsForScc(v, visited, component, sccId); |
| 240 | + } |
| 241 | + } |
| 242 | + } |
| 243 | + |
| 244 | + /** |
| 245 | + * Returns the index representing the negation of the given variable. |
| 246 | + * |
| 247 | + * <p> |
| 248 | + * Mapping rule: |
| 249 | + * </p> |
| 250 | + * |
| 251 | + * <pre> |
| 252 | + * For a variable i: |
| 253 | + * negate(i) = i + n |
| 254 | + * For a negated variable (i + n): |
| 255 | + * negate(i + n) = i |
| 256 | + * where n = numberOfVariables |
| 257 | + * </pre> |
| 258 | + * |
| 259 | + * @param a the variable index |
| 260 | + * @return the index representing its negation |
| 261 | + */ |
| 262 | + private int negate(int a) { |
| 263 | + return a <= numberOfVariables ? a + numberOfVariables : a - numberOfVariables; |
| 264 | + } |
| 265 | +} |
0 commit comments