What would you like to Propose?

I would like to propose adding an implementation of the 2-SAT (2-Satisfiability) problem to the graphs/ directory.

2-SAT is a special case of the Boolean Satisfiability (SAT) problem, where each clause contains at most two literals. While the general SAT problem is NP-complete, 2-SAT can be solved efficiently in polynomial time using graph algorithms — specifically, Strongly Connected Components (SCCs).

The implementation will:

• Take input as a set of variables and clauses.
• Construct an implication graph.
• Use SCC (Kosaraju’s or Tarjan’s algorithm) to determine satisfiability.
• Return whether the Boolean expression is satisfiable and, optionally, one satisfying assignment.

Issue details

Problem Description

• 2-SAT is special case of Boolean satisfiability(B-SAT) problem.
• The Boolean satisfiability problem is:
  • We have a Boolean expression in form of clauses($\lor$, $\land$, $\lnot$). We need to find the assignment to the Boolean variables such that is satisfies the Boolean expression.
  • More formally,
    • We have $n$ Boolean variables, $a_1, a_2, ..., a_n$ and the Boolean expression $F(a_1, a_2, ..., a_n)$ built using the variables , logical operators ($\land$, $\lor$ and $\lnot$) and parentheses, we need to find the assignment(true or false) for the given variables $a_1, a_2, a_3, ... , a_n$ which satisfies the Boolean expression ($F$).
• For example:
  • Boolean Expression: $$F(x_1, x_2, x_3) = ( x_1​\lor\lnot x_2​)\land(x_2​\lor x_3​)$$
  • Boolean Variables: $x_1, x_2, x_3$
  • One possible assignment can be: $x_1$​=True, $x_2$=False, $x_3$=True, put the variables in the expression and we get,
    $$F(t, f, t) = (t \lor t)\land(f\lor t) = t \lor t = t $$

Can we solve Boolean Satisfiability ?

• Actually the Satisfiability problem is proven to be NP-complete, but the special case of B-SAT can be solved in polynomial time.

2-SAT

• So in 2-SAT instead of any number of Boolean clause, we just have at most 2 Boolean clause and we can solve this efficiently using graph algorithms, to be more specific using Strongly Connected Component.
• Formally, we have $n$ variables and $m$ clauses,
  $$F=(a_1​∨b_1​)∧(a_2​∨b_2​)∧⋯∧(a_m∨b_m​)$$
• Where each $a_i$, $b_i$ is either variable $x_j$ or it's negation $x_j$
• Example of 2-SAT:
  • Expression
    $$F=(x_1​\lor x_2​)\land (\lnot x_1 ​\lor x_3​) \land (\lnot x_2 \lor \lnot x_3​)$$
  • One possible assignment : $x_1$​=t, $x_2$​ = f, $x_3$ ​=t
  • So above expression is giving true, on assigning a variable.

Testcase format

• We will be given $n$ and $m$, where $n$ is the number of boolean variables and $m$ is number of clauses(or expression).
• The next $m$ lines will contain the description of the each clause in following format:
  • $\pm$ a $\pm$ b
  • $a$ andn $b$ is the variable number, and $+$ means it's in original form and $-$ means the negation of $a_i^{th}$ variable.
• Example:

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

• From above testcase we have $3$ variables, $a_1, a_2, a_3$ and we can make following expression:

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

Purpose of this issue

• Add an efficient solution of the 2-SAT in /graphs directory(but I am not sure, should we include it in inside datastructure or graphs).
• The solution should:
  • Include detailed documentation and comments.
  • Clearly explain the SCC-based approach for checking satisfiability.
  • Include example test cases.

Additional Information

This is my first time submitting an issue. I’ve searched the repository (for “2-SAT”, “satisfiability”) and didn’t find an existing implementation. If it already exists, please feel free to close this issue. Thank you!