diff --git a/DIRECTORY.md b/DIRECTORY.md index b311b10fa..ff56d16db 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 000000000..835e38804 --- /dev/null +++ b/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. + * + *
+ * 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: + *
+ *+ * 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]);
+ * }
+ * }
+ *
+ * Reference
+ * CP Algorithm+ * 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
+ */
+ 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+ * 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 000000000..15e77b357 --- /dev/null +++ b/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."); + } +}