search

technojam / Ultimate_Algorithms_Repository

This is a collection of Data Structures and Algorithms
83 stars 166 forks source link

2-SAT Solver #293

Closed jatinAgarwala closed 4 years ago

jatinAgarwala commented 4 years ago

2-SAT Solver using Kosaraju's Algorithm

Description- Solving a 2-CNF formula (2-Satisfiability) by creating the corresponding implication graph, using Kosaraju's algorithm to find the Directly Connected Components (DCCs) and solving the 2-SAT

Examples-

Input : F = (x1 V x2) ^ (x2 V x1'}) ^ (x1' V x2') Output : The given expression is satisfiable. (for x1 = FALSE, x2 = TRUE)

Input : F = (x1V x2) ^ (x2 V x1') ^ (x1 V x2') ^ (x1' V x2') Output : The given expression is unsatisfiable. (for all possible combinations of x1 and x2)

jatinAgarwala commented 4 years ago

Please assign this to me.