How to get 2-Sat values

Question

Whenever I look for an algorithm for 2-Sat, I return an algorithm for the form to solve the problem: is there a legal set of values ​​that satisfy all the sentences. However, this does not allow me to easily find a set of satisfying Boolean values.

How can I effectively find a legitimate set of values ​​that will satisfy a 2-Sat instance?

I work in C ++ using the boost library and appreciate code that can be easily integrated.

Thanks in advance

Answer 1

If you have an algorithm for deciding whether there is a valid destination for 2-SAT, you can use it to actually determine the actual destination.

First run the 2-SAT solution algorithm for the entire expression. Suppose there is a valid destination.

Now, if x_1 is a literal, set x_1 to 0. Now calculate 2-SAT for the resulting expression (because of this, you will have to assign some other literals, for example, if x_1 OR x_3 appears, you also need to set x_3 to 1).

If the resulting expression is 2-Satisfactory, you can take x_1 to 0, otherwise take x_1 to 1.

Now you can learn about this every literal.

For a more efficient algorithm, I suggest you try using an implication approach.

You can find more information here: http://en.wikipedia.org/wiki/2-satisfiability

Relevant Part:

a 2-satisfiability instance is decidable if and only if each instance variable belongs to another strongly related component of the implication graph than the negation of the same variable. Since strongly coupled components can be found in linear time by an algorithm based on the depth of the first search, the same linear time reference also applies to 2-feasibility.

The literals in each strongly connected component are either all the same or all 1.

Answer 2

There is at least one algorithm that lists all solutions to the problem with two screens, Thomas Feder: http://www.springerlink.com/content/j582276p06276l12/