Hi I'm having trouble with the 2-CNF (Conjuctive Normal Form) problem, not just 2-SAT but the more general case of Conjuctive Normal Forms, ie :a => b (a implies b), c => ¬d (c implies not d). I've got some doubts, if you can help me with any of them it would help me a lot.

1 — What is the answer for the case (a => b) and (b => ¬a) and (¬a => c) and (c => d) and (d => ¬c)? I think its not satisfiable but some algorithms just get the variable with higher toposort between (x and ¬x).

2 — There is an algorithm to find if some 2-CNF is solvable? And if its solvable how can we get some solution.

3 -