Implementation issues in 2-Satisfiability problem

Question

I want to implement 2-SAT problem for 100000 literals. So there would be 200000 vertices. So I am stuck on having a array of all reachable vertices from each vertex, space complexity of O(200000^2) which is infeasible So please suggest a solution for this. And please throw some light on efficient implementation of 2-SAT problem.

Answer 1

From wikipedia:

... 2-satisfiability can be solved in polynomial time. As Aspvall, Plass & Tarjan (1979) observed, a 2-satisfiability instance is solvable if and only if every variable of the instance belongs to a different strongly connected component of the implication graph than the negation of the same variable. Since strongly connected components may be found in linear time by an algorithm based on depth first search, the same linear time bound applies as well to 2-satisfiability.

I won't pretend to understand most of that paragraph, but it would appear that there is an algorithm which can be used to solve the 2-SAT problem, and it is described within that referenced document (A linear-time algorithm for testing the truth of certain quantified boolean formulas). It can apparently be purchased online for about $20 USD. I'm Not sure if that's helpful or not, but there it is!

update: A free PDF of the same document can be found here. Credit goes to liori for the find.

Answer 2

This whole thread is a bit messed up. Yes, one can solve 2-sat in linear time, but no - you can not solve it for that many variables. The time to solve 2-sat is linear with respect to the number of the implication, which for 200 000 variables could reach up to (200000*199999)/2 and furthermore if you use this solution you will need about the same amount of memory. There is another solution(not using strongly connected components that is slower but doesn't need that much memory).