Skip to content

Commit 13d9fc2

Browse files
Shoyeb45Shoyeb45
committed
feat: added TwoSat solutions and Tests and also updated Directory.md
1 parent 69d8406 commit 13d9fc2

3 files changed

Lines changed: 387 additions & 0 deletions

File tree

‎DIRECTORY.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -173,6 +173,7 @@
173173
- 📄 [TarjansAlgorithm](src/main/java/com/thealgorithms/datastructures/graphs/TarjansAlgorithm.java)
174174
- 📄 [UndirectedAdjacencyListGraph](src/main/java/com/thealgorithms/datastructures/graphs/UndirectedAdjacencyListGraph.java)
175175
- 📄 [WelshPowell](src/main/java/com/thealgorithms/datastructures/graphs/WelshPowell.java)
176+
- 📄 [TwoSat](src/main/java/com/thealgorithms/datastructures/graphs/TwoSat.java)
176177
- 📁 **hashmap**
177178
- 📁 **hashing**
178179
- 📄 [GenericHashMapUsingArray](src/main/java/com/thealgorithms/datastructures/hashmap/hashing/GenericHashMapUsingArray.java)

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

Lines changed: 263 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,263 @@
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+
*
61+
* @author Shoyeb Ansari
62+
*
63+
* @see Kosaraju
64+
*/
65+
class TwoSat {
66+
67+
/** Number of variables in the boolean expression. */
68+
private final int numberOfVariables;
69+
70+
/** Implication graph built from the boolean clauses. */
71+
private final ArrayList<Integer>[] graph;
72+
73+
/** Transposed implication graph used in Kosaraju's algorithm. */
74+
private final ArrayList<Integer>[] graphTranspose;
75+
76+
/** Stores one valid truth assignment for all variables (1-indexed). */
77+
private final boolean[] variableAssignments;
78+
79+
/** Indicates whether a valid solution exists. */
80+
private boolean hasSolution = true;
81+
82+
/** Tracks whether the {@code solve()} method has been called. */
83+
private boolean isSolved = false;
84+
85+
/**
86+
* Initializes the TwoSat solver with the given number of variables.
87+
*
88+
* @param numberOfVariables the number of boolean variables
89+
* @throws IllegalArgumentException if the number of variables is negative
90+
*/
91+
@SuppressWarnings("unchecked")
92+
public TwoSat(int numberOfVariables) {
93+
if (numberOfVariables < 0) {
94+
throw new IllegalArgumentException("Number of variables cannot be negative.");
95+
}
96+
this.numberOfVariables = numberOfVariables;
97+
int n = 2 * numberOfVariables + 1;
98+
99+
graph = new ArrayList[n];
100+
graphTranspose = new ArrayList[n];
101+
for (int i = 0; i < n; i++) {
102+
graph[i] = new ArrayList<>();
103+
graphTranspose[i] = new ArrayList<>();
104+
}
105+
variableAssignments = new boolean[numberOfVariables + 1];
106+
}
107+
108+
/**
109+
* Adds a clause of the form (a ∨ b) to the boolean expression.
110+
*
111+
* <p>
112+
* Example: To add (¬x₁ ∨ x₂), call:
113+
* </p>
114+
*
115+
* <pre>{@code
116+
* addClause(1, true, 2, false);
117+
* }</pre>
118+
*
119+
* @param a the first variable (1 ≤ a ≤ numberOfVariables)
120+
* @param isNegateA {@code true} if variable {@code a} is negated
121+
* @param b the second variable (1 ≤ b ≤ numberOfVariables)
122+
* @param isNegateB {@code true} if variable {@code b} is negated
123+
* @throws IllegalArgumentException if {@code a} or {@code b} are out of range
124+
*/
125+
public void addClause(int a, boolean isNegateA, int b, boolean isNegateB) {
126+
if (a <= 0 || a > numberOfVariables) {
127+
throw new IllegalArgumentException("Variable number must be between 1 and " + numberOfVariables);
128+
}
129+
if (b <= 0 || b > numberOfVariables) {
130+
throw new IllegalArgumentException("Variable number must be between 1 and " + numberOfVariables);
131+
}
132+
133+
a = isNegateA ? negate(a) : a;
134+
b = isNegateB ? negate(b) : b;
135+
int notA = negate(a);
136+
int notB = negate(b);
137+
138+
// Add implications: (¬a → b) and (¬b → a)
139+
graph[notA].add(b);
140+
graph[notB].add(a);
141+
142+
// Build transpose graph
143+
graphTranspose[b].add(notA);
144+
graphTranspose[a].add(notB);
145+
}
146+
147+
/**
148+
* Solves the 2-SAT problem using Kosaraju's algorithm to find SCCs
149+
* and determines whether a satisfying assignment exists.
150+
*/
151+
public void solve() {
152+
isSolved = true;
153+
int n = 2 * numberOfVariables + 1;
154+
155+
boolean[] visited = new boolean[n];
156+
int[] component = new int[n];
157+
Stack<Integer> topologicalOrder = new Stack<>();
158+
159+
// Step 1: Perform DFS to get topological order
160+
for (int i = 1; i < n; i++) {
161+
if (!visited[i]) {
162+
dfsForTopologicalOrder(i, visited, topologicalOrder);
163+
}
164+
}
165+
166+
Arrays.fill(visited, false);
167+
int sccId = 0;
168+
169+
// Step 2: Find SCCs on transposed graph
170+
while (!topologicalOrder.isEmpty()) {
171+
int node = topologicalOrder.pop();
172+
if (!visited[node]) {
173+
dfsForScc(node, visited, component, sccId);
174+
sccId++;
175+
}
176+
}
177+
178+
// Step 3: Check for contradictions and assign values
179+
for (int i = 1; i <= numberOfVariables; i++) {
180+
int notI = negate(i);
181+
if (component[i] == component[notI]) {
182+
hasSolution = false;
183+
return;
184+
}
185+
// If SCC(i) > SCC(¬i), then variable i is true.
186+
variableAssignments[i] = component[i] > component[notI];
187+
}
188+
}
189+
190+
/**
191+
* Returns whether the given boolean formula is satisfiable.
192+
*
193+
* @return {@code true} if a solution exists; {@code false} otherwise
194+
* @throws Error if called before {@link #solve()}
195+
*/
196+
public boolean isSolutionExists() {
197+
if (!isSolved) {
198+
throw new Error("Please call solve() before checking for a solution.");
199+
}
200+
return hasSolution;
201+
}
202+
203+
/**
204+
* Returns one valid assignment of variables that satisfies the boolean formula.
205+
*
206+
* @return a boolean array where {@code result[i]} represents the truth value of
207+
* variable {@code xᵢ}
208+
* @throws Error if called before {@link #solve()} or if no solution exists
209+
*/
210+
public boolean[] getSolutions() {
211+
if (!isSolved) {
212+
throw new Error("Please call solve() before fetching the solution.");
213+
}
214+
if (!hasSolution) {
215+
throw new Error("No satisfying assignment exists for the given expression.");
216+
}
217+
return variableAssignments.clone();
218+
}
219+
220+
/** Performs DFS to compute topological order. */
221+
private void dfsForTopologicalOrder(int u, boolean[] visited, Stack<Integer> topologicalOrder) {
222+
visited[u] = true;
223+
for (int v : graph[u]) {
224+
if (!visited[v]) {
225+
dfsForTopologicalOrder(v, visited, topologicalOrder);
226+
}
227+
}
228+
topologicalOrder.push(u);
229+
}
230+
231+
/** Performs DFS on the transposed graph to identify SCCs. */
232+
private void dfsForScc(int u, boolean[] visited, int[] component, int sccId) {
233+
visited[u] = true;
234+
component[u] = sccId;
235+
for (int v : graphTranspose[u]) {
236+
if (!visited[v]) {
237+
dfsForScc(v, visited, component, sccId);
238+
}
239+
}
240+
}
241+
242+
/**
243+
* Returns the index representing the negation of the given variable.
244+
*
245+
* <p>
246+
* Mapping rule:
247+
* </p>
248+
*
249+
* <pre>
250+
* For a variable i:
251+
* negate(i) = i + n
252+
* For a negated variable (i + n):
253+
* negate(i + n) = i
254+
* where n = numberOfVariables
255+
* </pre>
256+
*
257+
* @param a the variable index
258+
* @return the index representing its negation
259+
*/
260+
private int negate(int a) {
261+
return a <= numberOfVariables ? a + numberOfVariables : a - numberOfVariables;
262+
}
263+
}

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

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
package com.thealgorithms.datastructures.graphs;
2+
3+
import static org.junit.jupiter.api.Assertions.*;
4+
5+
import org.junit.jupiter.api.Test;
6+
7+
/**
8+
* Testcases for 2-SAT.
9+
* Please note thea whlie checking for boolean assignments always keep n + 1 elements and the first element should be always false.
10+
*/
11+
public class TwoSatTest {
12+
private TwoSat twoSat;
13+
14+
/**
15+
* Case 1: Basic satisfiable case.
16+
* Simple 3 clauses with consistent assignments.
17+
*/
18+
@Test
19+
public void testSatisfiableBasicCase() {
20+
twoSat = new TwoSat(5);
21+
22+
twoSat.addClause(1, false, 2, false); // (x1 ∨ x2)
23+
twoSat.addClause(3, true, 2, false); // (¬x3 ∨ x2)
24+
twoSat.addClause(4, false, 5, true); // (x4 ∨ ¬x5)
25+
26+
twoSat.solve();
27+
28+
assertTrue(twoSat.isSolutionExists(), "Expected solution to exist");
29+
boolean[] expected = {false, true, true, true, true, true};
30+
assertArrayEquals(expected, twoSat.getSolutions());
31+
}
32+
33+
/**
34+
* Case 2: Unsatisfiable due to direct contradiction.
35+
* (x1 ∨ x1) ∧ (¬x1 ∨ ¬x1) makes x1 and ¬x1 both required.
36+
*/
37+
@Test
38+
public void testUnsatisfiableContradiction() {
39+
twoSat = new TwoSat(1);
40+
41+
twoSat.addClause(1, false, 1, false); // (x1 ∨ x1)
42+
twoSat.addClause(1, true, 1, true); // (¬x1 ∨ ¬x1)
43+
44+
twoSat.solve();
45+
46+
assertFalse(twoSat.isSolutionExists(), "Expected no solution (contradiction)");
47+
}
48+
49+
/**
50+
* Case 3: Single variable, trivially satisfiable.
51+
* Only (x1 ∨ x1) exists.
52+
*/
53+
@Test
54+
public void testSingleVariableTrivialSatisfiable() {
55+
twoSat = new TwoSat(1);
56+
57+
twoSat.addClause(1, false, 1, false); // (x1 ∨ x1)
58+
59+
twoSat.solve();
60+
61+
assertTrue(twoSat.isSolutionExists(), "Expected solution to exist");
62+
boolean[] expected = {false, true};
63+
assertArrayEquals(expected, twoSat.getSolutions());
64+
}
65+
66+
/**
67+
* Case 4: Larger satisfiable system with dependencies.
68+
* (x1 ∨ x2), (¬x2 ∨ x3), (¬x3 ∨ x4), (¬x4 ∨ x5)
69+
*/
70+
@Test
71+
public void testChainedDependenciesSatisfiable() {
72+
twoSat = new TwoSat(5);
73+
74+
twoSat.addClause(1, false, 2, false);
75+
twoSat.addClause(2, true, 3, false);
76+
twoSat.addClause(3, true, 4, false);
77+
twoSat.addClause(4, true, 5, false);
78+
79+
twoSat.solve();
80+
81+
assertTrue(twoSat.isSolutionExists(), "Expected solution to exist");
82+
boolean[] solution = twoSat.getSolutions();
83+
for (int i = 1; i <= 5; i++) {
84+
assertTrue(solution[i], "Expected x" + i + " to be true");
85+
}
86+
}
87+
88+
/**
89+
* Case 5: Contradiction due to dependency cycle.
90+
* (x1 ∨ x2), (¬x1 ∨ ¬x2), (x1 ∨ ¬x2), (¬x1 ∨ x2)
91+
* These clauses form a circular dependency making it impossible.
92+
*/
93+
@Test
94+
public void testUnsatisfiableCycle() {
95+
twoSat = new TwoSat(2);
96+
97+
twoSat.addClause(1, false, 2, false);
98+
twoSat.addClause(1, true, 2, true);
99+
twoSat.addClause(1, false, 2, true);
100+
twoSat.addClause(1, true, 2, false);
101+
102+
twoSat.solve();
103+
104+
assertFalse(twoSat.isSolutionExists(), "Expected no solution due to contradictory cycle");
105+
}
106+
107+
/**
108+
* Testcase from CSES
109+
*/
110+
@Test
111+
public void test6() {
112+
twoSat = new TwoSat(2);
113+
114+
twoSat.addClause(1, true, 2, false);
115+
twoSat.addClause(2, true, 1, false);
116+
twoSat.addClause(1, true, 1, true);
117+
twoSat.addClause(2, false, 2, false);
118+
119+
twoSat.solve();
120+
121+
assertFalse(twoSat.isSolutionExists(), "Expected no solution.");
122+
}
123+
}

0 commit comments

Comments
 (0)