Whenever I search for an algorithm for 2-Sat, I get back the algorithm for the decision form of the problem: Does there exist a legal set of values that satisfy all the clauses. However, that does not allow me to easily find a set of satisfying boolean values.
How can I efficiently find a legal set of values that will satisfy a 2-Sat instance?
I am working in c++ with the boost library and would appreciate code that can be easily integrated.
Thanks in advance
There's at least one algorithm that lists all the solutions to a 2-sat problem, by Tomas Feder: http://www.springerlink.com/content/j582276p06276l12/
If you have a decision algorithm for detecting if there exists a valid assignment to 2-SAT, you can use that to actually find out the actual assignment.
First run 2-SAT decision algorithm on the whole expression. Assume it says there is a valid assignment.
Now if x_1 is a literal, Assign x_1 to be 0. Now compute the 2-SAT for the resulting expression (you will have to assign some other literals because of this, for instance if x_1 OR x_3 appears, you also need to set x_3 to 1).
If the resulting expresion is 2-Satisfiable, then you can take x_1 to be 0, else take x_1 to 1.
Now you can find this out about each literal.
For a more efficient algorithm, I would suggest you try using the implication graph approach.
You can find more info here: http://en.wikipedia.org/wiki/2-satisfiability
The relevant portion:
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.
The literals in each strongly connected component are either all zero or all 1.