From 13d9fc201c1fa9e346185f0332f303f867613e36 Mon Sep 17 00:00:00 2001 From: Shoyeb45 Date: Sun, 12 Oct 2025 16:21:27 +0530 Subject: [PATCH 1/6] feat: added TwoSat solutions and Tests and also updated Directory.md --- DIRECTORY.md | 1 + .../datastructures/graphs/TwoSat.java | 263 ++++++++++++++++++ .../datastructures/graphs/TwoSatTest.java | 123 ++++++++ 3 files changed, 387 insertions(+) create mode 100644 src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java create mode 100644 src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java diff --git a/DIRECTORY.md b/DIRECTORY.md index b311b10fa177..ff56d16db947 100644 --- a/DIRECTORY.md +++ b/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) diff --git a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java new file mode 100644 index 000000000000..ea1a7b5acad7 --- /dev/null +++ b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java @@ -0,0 +1,263 @@ +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. + * + *

+ * Brief Idea: + *

+ * + * 
+ * 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.
+ *
+ * + *

+ * Complexities: + *

+ * + * where {@code n} is the number of variables and {@code m} is the number of + * clauses. + * + *

+ * Usage Example: + *

+ * + * 
+ * 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]);
+ *     }
+ * }
+ *
+ * + * @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[] graph; + + /** Transposed implication graph used in Kosaraju's algorithm. */ + private final ArrayList[] 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") + public TwoSat(int numberOfVariables) { + if (numberOfVariables < 0) { + throw new IllegalArgumentException("Number of variables cannot be negative."); + } + this.numberOfVariables = numberOfVariables; + int n = 2 * numberOfVariables + 1; + + graph = new ArrayList[n]; + graphTranspose = 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. + * + *

+ * Example: To add (¬x₁ ∨ x₂), call: + *

+ * + * 
{@code
+     * addClause(1, true, 2, false);
+     * }
+ * + * @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 + */ + public 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. + */ + public void solve() { + isSolved = true; + int n = 2 * numberOfVariables + 1; + + boolean[] visited = new boolean[n]; + int[] component = new int[n]; + Stack 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()} + */ + public 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 + */ + public 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 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. + * + *

+ * Mapping rule: + *

+ * + * 
+     * For a variable i:
+     *     negate(i) = i + n
+     * For a negated variable (i + n):
+     *     negate(i + n) = i
+     * where n = numberOfVariables
+     *
+ * + * @param a the variable index + * @return the index representing its negation + */ + private int negate(int a) { + return a <= numberOfVariables ? a + numberOfVariables : a - numberOfVariables; + } +} diff --git a/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java b/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java new file mode 100644 index 000000000000..41d364aedb0b --- /dev/null +++ b/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java @@ -0,0 +1,123 @@ +package com.thealgorithms.datastructures.graphs; + +import static org.junit.jupiter.api.Assertions.*; + +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."); + } +} From 05cf9c19f6c6d4185ac3bc80edab2dd30c7662ec Mon Sep 17 00:00:00 2001 From: Shoyeb45 Date: Sun, 12 Oct 2025 16:30:54 +0530 Subject: [PATCH 2/6] added reference urls to the article related to the 2-SAT --- .../java/com/thealgorithms/datastructures/graphs/TwoSat.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java index ea1a7b5acad7..7c91fe2d1df0 100644 --- a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java +++ b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java @@ -57,7 +57,9 @@ * } * } * - * + *

Reference

+ * CP Algorithm

+ * Wikipedia - 2 SAT * @author Shoyeb Ansari * * @see Kosaraju From 1aec66f2ccaff5be30fbf725d9efb27dba6426cc Mon Sep 17 00:00:00 2001 From: Shoyeb45 Date: Sun, 12 Oct 2025 16:35:54 +0530 Subject: [PATCH 3/6] Fix generic type warnings in TwoSat.java --- .../java/com/thealgorithms/datastructures/graphs/TwoSat.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java index 7c91fe2d1df0..6c8857ef12c8 100644 --- a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java +++ b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java @@ -98,8 +98,8 @@ public TwoSat(int numberOfVariables) { this.numberOfVariables = numberOfVariables; int n = 2 * numberOfVariables + 1; - graph = new ArrayList[n]; - graphTranspose = new ArrayList[n]; + graph = (ArrayList[]) new ArrayList[n]; + graphTranspose = (ArrayList[]) new ArrayList[n]; for (int i = 0; i < n; i++) { graph[i] = new ArrayList<>(); graphTranspose[i] = new ArrayList<>(); From 001e441b1388a9948368914a553eeb42d73bebf9 Mon Sep 17 00:00:00 2001 From: Shoyeb45 Date: Sun, 12 Oct 2025 17:08:18 +0530 Subject: [PATCH 4/6] maven build fix: added rawtypes in SuppressWarnings --- .../java/com/thealgorithms/datastructures/graphs/TwoSat.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java index 6c8857ef12c8..1028139776b5 100644 --- a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java +++ b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java @@ -90,7 +90,7 @@ class TwoSat { * @param numberOfVariables the number of boolean variables * @throws IllegalArgumentException if the number of variables is negative */ - @SuppressWarnings("unchecked") + @SuppressWarnings({"unchecked", "rawtypes"}) public TwoSat(int numberOfVariables) { if (numberOfVariables < 0) { throw new IllegalArgumentException("Number of variables cannot be negative."); From 873428c968db78bd111a63316b219aff97df0aa3 Mon Sep 17 00:00:00 2001 From: Shoyeb45 Date: Sun, 12 Oct 2025 17:31:45 +0530 Subject: [PATCH 5/6] fixed checkstyle error --- .../thealgorithms/datastructures/graphs/TwoSat.java | 10 +++++----- .../datastructures/graphs/TwoSatTest.java | 4 +++- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java index 1028139776b5..835e3880428f 100644 --- a/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java +++ b/src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java @@ -91,7 +91,7 @@ class TwoSat { * @throws IllegalArgumentException if the number of variables is negative */ @SuppressWarnings({"unchecked", "rawtypes"}) - public TwoSat(int numberOfVariables) { + TwoSat(int numberOfVariables) { if (numberOfVariables < 0) { throw new IllegalArgumentException("Number of variables cannot be negative."); } @@ -124,7 +124,7 @@ public TwoSat(int numberOfVariables) { * @param isNegateB {@code true} if variable {@code b} is negated * @throws IllegalArgumentException if {@code a} or {@code b} are out of range */ - public void addClause(int a, boolean isNegateA, int b, boolean isNegateB) { + 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); } @@ -150,7 +150,7 @@ public void addClause(int a, boolean isNegateA, int b, boolean isNegateB) { * Solves the 2-SAT problem using Kosaraju's algorithm to find SCCs * and determines whether a satisfying assignment exists. */ - public void solve() { + void solve() { isSolved = true; int n = 2 * numberOfVariables + 1; @@ -195,7 +195,7 @@ public void solve() { * @return {@code true} if a solution exists; {@code false} otherwise * @throws Error if called before {@link #solve()} */ - public boolean isSolutionExists() { + boolean isSolutionExists() { if (!isSolved) { throw new Error("Please call solve() before checking for a solution."); } @@ -209,7 +209,7 @@ public boolean isSolutionExists() { * variable {@code xᵢ} * @throws Error if called before {@link #solve()} or if no solution exists */ - public boolean[] getSolutions() { + boolean[] getSolutions() { if (!isSolved) { throw new Error("Please call solve() before fetching the solution."); } diff --git a/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java b/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java index 41d364aedb0b..2c9bef884aeb 100644 --- a/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java +++ b/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java @@ -1,6 +1,8 @@ package com.thealgorithms.datastructures.graphs; -import static org.junit.jupiter.api.Assertions.*; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertTrue; +import static org.junit.jupiter.api.Assertions.assertArrayEquals; import org.junit.jupiter.api.Test; From 9b47ea25e057c76f7a4228dc9b964b7f2d70affc Mon Sep 17 00:00:00 2001 From: Shoyeb45 Date: Sun, 12 Oct 2025 17:53:21 +0530 Subject: [PATCH 6/6] fix: Sorted import order --- .../com/thealgorithms/datastructures/graphs/TwoSatTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java b/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java index 2c9bef884aeb..15e77b357f83 100644 --- a/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java +++ b/src/test/java/com/thealgorithms/datastructures/graphs/TwoSatTest.java @@ -1,8 +1,8 @@ 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 static org.junit.jupiter.api.Assertions.assertArrayEquals; import org.junit.jupiter.api.Test;