2-SAT Implementation In Graphs: A Feature Request

Oct 12, 2025 by ADMIN 50 views

Hey guys! I'm excited to propose a cool new feature for TheAlgorithms/Java: implementing the 2-SAT (2-Satisfiability) problem within the graphs/ directory. This addition would be super valuable, offering an efficient solution to a specific type of Boolean satisfiability problem. Let's dive into the details!

What is 2-SAT?

Problem Description

2-SAT is a special, more manageable case of the broader Boolean Satisfiability (B-SAT) problem. To understand 2-SAT, it's essential to first grasp what Boolean Satisfiability is all about. At its core, the Boolean Satisfiability problem deals with determining whether there exists an assignment of truth values to the variables of a Boolean expression that makes the entire expression true.

Think of it this way: You're given a Boolean expression constructed from variables, logical operators (like AND, OR, and NOT), and parentheses. The challenge is to find a combination of true and false values for the variables that makes the entire expression evaluate to true. More formally, imagine you have $n$ Boolean variables, denoted as $a_1, a_2, ..., a_n$ . The Boolean expression, represented as $F(a_1, a_2, ..., a_n)$ , is built using these variables, logical operators ( $\land$ , $\lor$ , and $\lnot$ ), and parentheses. The goal is to find an assignment (either true or false) for each of these variables such that the entire Boolean expression $F$ evaluates to true.

For example, consider a Boolean expression like this:

F(x_1, x_2, x_3) = ( x_1 \lor \lnot x_2) \land (x_2 \lor x_3)

In this case, the Boolean variables are $x_1, x_2,$ and $x_3$ . One possible assignment could be:

$x_1$ = True, $x_2$ = False, $x_3$ = True

Plugging these values into the expression, we get:

F(t, f, t) = (t \lor t) \land (f \lor t) = t \land t = t

Since the expression evaluates to true with this assignment, it satisfies the Boolean expression.

Can we solve Boolean Satisfiability?

Solving the general Satisfiability problem is known to be NP-complete, which implies that finding a solution can be computationally expensive for large expressions. However, the good news is that the special case of 2-SAT can be solved in polynomial time, making it much more practical for certain applications.

Diving into 2-SAT

2-SAT is a specific type of Boolean satisfiability problem where each clause in the expression contains at most two literals. This constraint allows us to solve 2-SAT efficiently using graph algorithms, particularly by leveraging Strongly Connected Components (SCCs).

Formally, we have $n$ variables and $m$ clauses, expressed as:

F=(a_1 \lor b_1) \land (a_2 \lor b_2) \land \cdots \land (a_m \lor b_m)

Where each $a_i$ and $b_i$ is either a variable $x_j$ or its negation $\lnot x_j$ .

Consider the following 2-SAT expression as an example:

F=(x_1 \lor x_2) \land (\lnot x_1 \lor x_3) \land (\lnot x_2 \lor \lnot x_3)

One possible assignment that satisfies this expression is:

$x_1$ = true, $x_2$ = false, $x_3$ = true

Assigning these values to the variables makes the entire expression evaluate to true.

Testcase Format

When dealing with 2-SAT problems, the input format typically follows a specific structure. You'll be given two integers, $n$ and $m$ , where $n$ represents the number of Boolean variables and $m$ represents the number of clauses (or expressions).

The subsequent $m$ lines will describe each clause in the following format:

$\pm$ a $\pm$ b

Here, $a$ and $b$ represent the variable numbers, and the $\pm$ signs indicate whether the variable appears in its original form (+) or as its negation (-). Let's illustrate this with an example:

5 3
+ 1 + 2
- 1 + 3
+ 4 - 2

In this test case, we have 5 variables ( $x_1, x_2, x_3, x_4, x_5$ ) and 3 clauses. We can represent these clauses in the following expression:

F = (x_1 \lor x_2) \land (\lnot x_1 \lor x_3) \land (x_4 \lor \lnot x_2)

Proposed Implementation

The goal is to add an efficient solution for 2-SAT to the /graphs directory. The solution should:

Include detailed documentation and comments to ensure clarity and understanding.
Clearly explain the SCC-based approach used for checking satisfiability. This is the crux of the algorithm, so a good explanation is essential.
Include example test cases to demonstrate the functionality and correctness of the implementation.

Why this is awesome!

Educational Resource: A 2-SAT implementation would serve as an excellent educational resource, helping users understand graph algorithms and their applications.
Practical Usefulness: 2-SAT solvers have practical applications in various fields, such as software verification, planning, and constraint satisfaction.
Completeness: Adding this implementation would enhance the completeness of the algorithms library, making it an even more valuable resource for developers and students.

How it Works: Implication Graphs and SCCs

The beauty of solving 2-SAT lies in its clever reduction to a graph problem. Here's the gist:

Implication Graph: We transform the 2-SAT formula into a directed graph called an implication graph. For each clause (a ∨ b), we add two directed edges: ¬a → b and ¬b → a. Think of these edges as "if not a, then b" and "if not b, then a".
Strongly Connected Components (SCCs): We find the SCCs in this implication graph. An SCC is a set of nodes where you can reach any node from any other node within the set.
Satisfiability Check: The 2-SAT instance is satisfiable if and only if for each variable x, x and ¬x do not belong to the same SCC. If they do, it means we have a contradiction: if x is true, then ¬x must be true, and vice versa, which is impossible.
Finding an Assignment (Optional): If the instance is satisfiable, we can find a satisfying assignment by assigning values to the variables based on the topological order of the SCCs. Variables in SCCs that appear later in the topological order are assigned values first.

Algorithms to Use

For finding SCCs, we can use either:

Kosaraju's Algorithm: This algorithm performs two Depth-First Searches (DFS). The first DFS computes the finishing times of each vertex. The second DFS is performed on the transpose graph (reversed edges) in the order of decreasing finishing times.
Tarjan's Algorithm: This algorithm uses a single DFS to find SCCs. It maintains a stack of vertices and uses low-link values to identify SCCs.

Both algorithms have a time complexity of O(V + E), where V is the number of vertices (variables and their negations) and E is the number of edges in the implication graph.

Test Case Example and Explanation

Let's walk through an example to solidify the concept. Consider the following 2-SAT expression:

(x ∨ y) ∧ (¬x ∨ z) ∧ (¬y ∨ ¬z)

Implication Graph:
- x ∨ y => ¬x → y and ¬y → x
- ¬x ∨ z => x → z and ¬z → ¬x
- ¬y ∨ ¬z => y → ¬z and z → ¬y
SCCs: After constructing the implication graph and running an SCC algorithm (like Kosaraju's or Tarjan's), we identify the strongly connected components. Let's say we find the following SCCs (this is just an example, the actual SCCs depend on the specific graph structure):
- {x}
- {y}
- {z}
- {¬x, ¬z, ¬y}
Satisfiability Check: Notice that x and ¬x are in different SCCs. The same is true for y and ¬y, and z and ¬z. Therefore, the expression is satisfiable!
Finding an Assignment: To find a satisfying assignment, we consider the topological order of the SCCs. In this example (and this is a highly simplified example for illustration), let's say the topological order is:
- {¬x, ¬z, ¬y}
- {z}
- {y}
- {x}
We assign values to the variables in the reverse topological order. So, we start with x. Since the SCC {x} comes last, we can assign x = true (or false, it doesn't matter at this point). Then, we move to y, then z, and finally ¬x, ¬y, and ¬z. We need to make sure our assignments are consistent. If we assigned x = true, then we must assign ¬x = false.

One possible satisfying assignment is: x = true, y = false, z = true.

Another Test Case

Consider the following 2-SAT expression:

(x ∨ y) ∧ (¬x ∨ y) ∧ (¬y ∨ x) ∧ (¬x ∨ ¬y)

Implication Graph:
- x ∨ y => ¬x → y and ¬y → x
- ¬x ∨ y => x → y and ¬y → ¬x
- ¬y ∨ x => y → x and ¬x → ¬y
- ¬x ∨ ¬y => x → ¬y and y → ¬x
SCCs: After constructing the implication graph and running an SCC algorithm, we might find the following SCCs:
- {x, ¬x, y, ¬y}
Satisfiability Check: Notice that x and ¬x are in the same SCC! This means there's a contradiction, and the expression is not satisfiable.

Purpose of this issue

I'm opening this issue to propose the addition of an efficient 2-SAT solver to the /graphs directory (though I'm open to suggestions on whether it might be better placed within /datastructures). The implementation should include:

Well-documented code with clear comments.
A comprehensive explanation of the SCC-based approach.
Example test cases to ensure correctness.

Additional Information

This is my first time submitting an issue, so please bear with me! I've searched the repository for existing 2-SAT implementations but haven't found one. If one already exists, please feel free to close this issue. Thanks for considering this feature request! I believe it would be a valuable addition to the library.