2-Satisfiability and Strongly connected components

Question

I know that applying Strongly connected components in a Digraph we can check 2-SAT boolean satisfiability if the problem is solvable in polynomial time.

Let's assume the problem is satisfiable.

The question: is there a general algorithm to calculate that solution relying on 2-SAT?

Answer 1

Assuming I understand your question correctly, yes, there is a general algorithm to find a solution (i.e. a satisfying assignment) by using the algorithm for the satisfiability problem.

Suppose I assign a variable x_i the value "true" (so that the literal x_i is true and ~x_i is false) to make a new 2-CNF from the original. If I were to run satisfiability on it (i.e. use the thing with SCCs to find if the new CNF is satisfiable):

1. What does it tell you about the satisfying assignments in the original CNF if the resulting CNF is now not satisfiable?
2. What does it tell you about the satisfying assignments in the original CNF if the resulting CNF is still satisfiable?

The idea behind the algorithm is to make the variable "false" if you hit case 1, and "true" if you hit case 2, and loop through every variable (keeping the assignments that you made to variables you've already looked at). Once you can answer the questions I've posed, you'll understand the concept behind it.