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
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:
The literals in each strongly connected component are either all zero or all 1.