feat: added TwoSat solutions with Tests, also updated Directory.md

DIRECTORY.md

@@ -173,6 +173,7 @@
             - 📄 [TarjansAlgorithm](src/main/java/com/thealgorithms/datastructures/graphs/TarjansAlgorithm.java)
             - 📄 [UndirectedAdjacencyListGraph](src/main/java/com/thealgorithms/datastructures/graphs/UndirectedAdjacencyListGraph.java)
             - 📄 [WelshPowell](src/main/java/com/thealgorithms/datastructures/graphs/WelshPowell.java)
+            - 📄 [TwoSat](src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java)
           - 📁 **hashmap**
             - 📁 **hashing**
               - 📄 [GenericHashMapUsingArray](src/main/java/com/thealgorithms/datastructures/hashmap/hashing/GenericHashMapUsingArray.java)

src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java

@@ -0,0 +1,265 @@
+package com.thealgorithms.datastructures.graphs;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Stack;
+
+/**
+ * This class implements a solution to the 2-SAT (2-Satisfiability) problem
+ * using Kosaraju's algorithm to find strongly connected components (SCCs)
+ * in the implication graph.
+ *
+ * <p>
+ * <strong>Brief Idea:</strong>
+ * </p>
+ *
+ * <pre>
+ * 1. From each clause (a ∨ b), we can derive implications:
+ *      (¬a → b) and (¬b → a)
+ *
+ * 2. We construct an implication graph using these implications.
+ *
+ * 3. For each variable x, its negation ¬x is also represented as a node.
+ *    If x and ¬x belong to the same SCC, the expression is unsatisfiable.
+ *
+ * 4. Otherwise, we assign truth values based on the SCC order:
+ *    If SCC(x) > SCC(¬x), then x = true; otherwise, x = false.
+ * </pre>
+ *
+ * <p>
+ * <strong>Complexities:</strong>
+ * </p>
+ * <ul>
+ * <li>Time Complexity: O(n + m)</li>
+ * <li>Space Complexity: O(n + m)</li>
+ * </ul>
+ * where {@code n} is the number of variables and {@code m} is the number of
+ * clauses.
+ *
+ * <p>
+ * <strong>Usage Example:</strong>
+ * </p>
+ *
+ * <pre>
+ * TwoSat twoSat = new TwoSat(5); // Initialize with 5 variables: x1, x2, x3, x4, x5
+ *
+ * // Add clauses
+ * twoSat.addClause(1, false, 2, false); // (x1 ∨ x2)
+ * twoSat.addClause(3, true, 2, false); // (¬x3 ∨ x2)
+ * twoSat.addClause(4, false, 5, true); // (x4 ∨ ¬x5)
+ *
+ * twoSat.solve(); // Solve the problem
+ *
+ * if (twoSat.isSolutionExists()) {
+ *     boolean[] solution = twoSat.getSolutions();
+ *     for (int i = 1; i <= 5; i++) {
+ *         System.out.println("x" + i + " = " + solution[i]);
+ *     }
+ * }
+ * </pre>
+ * <p><strong>Reference</strong></p>
+ * <a href="https://cp-algorithms.com/graph/2SAT.html">CP Algorithm</a> <br></br>
+ * <a href="https://en.wikipedia.org/wiki/2-satisfiability">Wikipedia - 2 SAT</a>
+ * @author Shoyeb Ansari
+ *
+ * @see Kosaraju
+ */
+class TwoSat {
+
+    /** Number of variables in the boolean expression. */
+    private final int numberOfVariables;
+
+    /** Implication graph built from the boolean clauses. */
+    private final ArrayList<Integer>[] graph;
+
+    /** Transposed implication graph used in Kosaraju's algorithm. */
+    private final ArrayList<Integer>[] graphTranspose;
+
+    /** Stores one valid truth assignment for all variables (1-indexed). */
+    private final boolean[] variableAssignments;
+
+    /** Indicates whether a valid solution exists. */
+    private boolean hasSolution = true;
+
+    /** Tracks whether the {@code solve()} method has been called. */
+    private boolean isSolved = false;
+
+    /**
+     * Initializes the TwoSat solver with the given number of variables.
+     *
+     * @param numberOfVariables the number of boolean variables
+     * @throws IllegalArgumentException if the number of variables is negative
+     */
+    @SuppressWarnings({"unchecked", "rawtypes"})
+    TwoSat(int numberOfVariables) {
+        if (numberOfVariables < 0) {
+            throw new IllegalArgumentException("Number of variables cannot be negative.");
+        }
+        this.numberOfVariables = numberOfVariables;
+        int n = 2 * numberOfVariables + 1;
+
+        graph = (ArrayList<Integer>[]) new ArrayList[n];
+        graphTranspose = (ArrayList<Integer>[]) new ArrayList[n];
+        for (int i = 0; i < n; i++) {
+            graph[i] = new ArrayList<>();
+            graphTranspose[i] = new ArrayList<>();
+        }
+        variableAssignments = new boolean[numberOfVariables + 1];
+    }
+
+    /**
+     * Adds a clause of the form (a ∨ b) to the boolean expression.
+     *
+     * <p>
+     * Example: To add (¬x₁ ∨ x₂), call:
+     * </p>
+     *
+     * <pre>{@code
+     * addClause(1, true, 2, false);
+     * }</pre>
+     *
+     * @param a         the first variable (1 ≤ a ≤ numberOfVariables)
+     * @param isNegateA {@code true} if variable {@code a} is negated
+     * @param b         the second variable (1 ≤ b ≤ numberOfVariables)
+     * @param isNegateB {@code true} if variable {@code b} is negated
+     * @throws IllegalArgumentException if {@code a} or {@code b} are out of range
+     */
+    void addClause(int a, boolean isNegateA, int b, boolean isNegateB) {
+        if (a <= 0 || a > numberOfVariables) {
+            throw new IllegalArgumentException("Variable number must be between 1 and " + numberOfVariables);
+        }
+        if (b <= 0 || b > numberOfVariables) {
+            throw new IllegalArgumentException("Variable number must be between 1 and " + numberOfVariables);
+        }
+
+        a = isNegateA ? negate(a) : a;
+        b = isNegateB ? negate(b) : b;
+        int notA = negate(a);
+        int notB = negate(b);
+
+        // Add implications: (¬a → b) and (¬b → a)
+        graph[notA].add(b);
+        graph[notB].add(a);
+
+        // Build transpose graph
+        graphTranspose[b].add(notA);
+        graphTranspose[a].add(notB);
+    }
+
+    /**
+     * Solves the 2-SAT problem using Kosaraju's algorithm to find SCCs
+     * and determines whether a satisfying assignment exists.
+     */
+    void solve() {
+        isSolved = true;
+        int n = 2 * numberOfVariables + 1;
+
+        boolean[] visited = new boolean[n];
+        int[] component = new int[n];
+        Stack<Integer> topologicalOrder = new Stack<>();
+
+        // Step 1: Perform DFS to get topological order
+        for (int i = 1; i < n; i++) {
+            if (!visited[i]) {
+                dfsForTopologicalOrder(i, visited, topologicalOrder);
+            }
+        }
+
+        Arrays.fill(visited, false);
+        int sccId = 0;
+
+        // Step 2: Find SCCs on transposed graph
+        while (!topologicalOrder.isEmpty()) {
+            int node = topologicalOrder.pop();
+            if (!visited[node]) {
+                dfsForScc(node, visited, component, sccId);
+                sccId++;
+            }
+        }
+
+        // Step 3: Check for contradictions and assign values
+        for (int i = 1; i <= numberOfVariables; i++) {
+            int notI = negate(i);
+            if (component[i] == component[notI]) {
+                hasSolution = false;
+                return;
+            }
+            // If SCC(i) > SCC(¬i), then variable i is true.
+            variableAssignments[i] = component[i] > component[notI];
+        }
+    }
+
+    /**
+     * Returns whether the given boolean formula is satisfiable.
+     *
+     * @return {@code true} if a solution exists; {@code false} otherwise
+     * @throws Error if called before {@link #solve()}
+     */
+    boolean isSolutionExists() {
+        if (!isSolved) {
+            throw new Error("Please call solve() before checking for a solution.");
+        }
+        return hasSolution;
+    }
+
+    /**
+     * Returns one valid assignment of variables that satisfies the boolean formula.
+     *
+     * @return a boolean array where {@code result[i]} represents the truth value of
+     *         variable {@code xᵢ}
+     * @throws Error if called before {@link #solve()} or if no solution exists
+     */
+    boolean[] getSolutions() {
+        if (!isSolved) {
+            throw new Error("Please call solve() before fetching the solution.");
+        }
+        if (!hasSolution) {
+            throw new Error("No satisfying assignment exists for the given expression.");
+        }
+        return variableAssignments.clone();
+    }
+
+    /** Performs DFS to compute topological order. */
+    private void dfsForTopologicalOrder(int u, boolean[] visited, Stack<Integer> topologicalOrder) {
+        visited[u] = true;
+        for (int v : graph[u]) {
+            if (!visited[v]) {
+                dfsForTopologicalOrder(v, visited, topologicalOrder);
+            }
+        }
+        topologicalOrder.push(u);
+    }
+
+    /** Performs DFS on the transposed graph to identify SCCs. */
+    private void dfsForScc(int u, boolean[] visited, int[] component, int sccId) {
+        visited[u] = true;
+        component[u] = sccId;
+        for (int v : graphTranspose[u]) {
+            if (!visited[v]) {
+                dfsForScc(v, visited, component, sccId);
+            }
+        }
+    }
+
+    /**
+     * Returns the index representing the negation of the given variable.
+     *
+     * <p>
+     * Mapping rule:
+     * </p>
+     *
+     * <pre>
+     * For a variable i:
+     *     negate(i) = i + n
+     * For a negated variable (i + n):
+     *     negate(i + n) = i
+     * where n = numberOfVariables
+     * </pre>
+     *
+     * @param a the variable index
+     * @return the index representing its negation
+     */
+    private int negate(int a) {
+        return a <= numberOfVariables ? a + numberOfVariables : a - numberOfVariables;
+    }
+}

src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java

@@ -0,0 +1,125 @@
+package com.thealgorithms.datastructures.graphs;
+
+import static org.junit.jupiter.api.Assertions.assertArrayEquals;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import org.junit.jupiter.api.Test;
+
+/**
+ * Testcases for 2-SAT.
+ * Please note thea whlie checking for boolean assignments always keep n + 1 elements and the first element should be always false.
+ */
+public class TwoSatTest {
+    private TwoSat twoSat;
+
+    /**
+     * Case 1: Basic satisfiable case.
+     * Simple 3 clauses with consistent assignments.
+     */
+    @Test
+    public void testSatisfiableBasicCase() {
+        twoSat = new TwoSat(5);
+
+        twoSat.addClause(1, false, 2, false); // (x1 ∨ x2)
+        twoSat.addClause(3, true, 2, false); // (¬x3 ∨ x2)
+        twoSat.addClause(4, false, 5, true); // (x4 ∨ ¬x5)
+
+        twoSat.solve();
+
+        assertTrue(twoSat.isSolutionExists(), "Expected solution to exist");
+        boolean[] expected = {false, true, true, true, true, true};
+        assertArrayEquals(expected, twoSat.getSolutions());
+    }
+
+    /**
+     * Case 2: Unsatisfiable due to direct contradiction.
+     * (x1 ∨ x1) ∧ (¬x1 ∨ ¬x1) makes x1 and ¬x1 both required.
+     */
+    @Test
+    public void testUnsatisfiableContradiction() {
+        twoSat = new TwoSat(1);
+
+        twoSat.addClause(1, false, 1, false); // (x1 ∨ x1)
+        twoSat.addClause(1, true, 1, true); // (¬x1 ∨ ¬x1)
+
+        twoSat.solve();
+
+        assertFalse(twoSat.isSolutionExists(), "Expected no solution (contradiction)");
+    }
+
+    /**
+     * Case 3: Single variable, trivially satisfiable.
+     * Only (x1 ∨ x1) exists.
+     */
+    @Test
+    public void testSingleVariableTrivialSatisfiable() {
+        twoSat = new TwoSat(1);
+
+        twoSat.addClause(1, false, 1, false); // (x1 ∨ x1)
+
+        twoSat.solve();
+
+        assertTrue(twoSat.isSolutionExists(), "Expected solution to exist");
+        boolean[] expected = {false, true};
+        assertArrayEquals(expected, twoSat.getSolutions());
+    }
+
+    /**
+     * Case 4: Larger satisfiable system with dependencies.
+     * (x1 ∨ x2), (¬x2 ∨ x3), (¬x3 ∨ x4), (¬x4 ∨ x5)
+     */
+    @Test
+    public void testChainedDependenciesSatisfiable() {
+        twoSat = new TwoSat(5);
+
+        twoSat.addClause(1, false, 2, false);
+        twoSat.addClause(2, true, 3, false);
+        twoSat.addClause(3, true, 4, false);
+        twoSat.addClause(4, true, 5, false);
+
+        twoSat.solve();
+
+        assertTrue(twoSat.isSolutionExists(), "Expected solution to exist");
+        boolean[] solution = twoSat.getSolutions();
+        for (int i = 1; i <= 5; i++) {
+            assertTrue(solution[i], "Expected x" + i + " to be true");
+        }
+    }
+
+    /**
+     * Case 5: Contradiction due to dependency cycle.
+     * (x1 ∨ x2), (¬x1 ∨ ¬x2), (x1 ∨ ¬x2), (¬x1 ∨ x2)
+     * These clauses form a circular dependency making it impossible.
+     */
+    @Test
+    public void testUnsatisfiableCycle() {
+        twoSat = new TwoSat(2);
+
+        twoSat.addClause(1, false, 2, false);
+        twoSat.addClause(1, true, 2, true);
+        twoSat.addClause(1, false, 2, true);
+        twoSat.addClause(1, true, 2, false);
+
+        twoSat.solve();
+
+        assertFalse(twoSat.isSolutionExists(), "Expected no solution due to contradictory cycle");
+    }
+
+    /**
+     * Testcase from CSES
+     */
+    @Test
+    public void test6() {
+        twoSat = new TwoSat(2);
+
+        twoSat.addClause(1, true, 2, false);
+        twoSat.addClause(2, true, 1, false);
+        twoSat.addClause(1, true, 1, true);
+        twoSat.addClause(2, false, 2, false);
+
+        twoSat.solve();
+
+        assertFalse(twoSat.isSolutionExists(), "Expected no solution.");
+    }
+}