2 satisfiability strongly connected components topological ordering

Question

I'm solving a two-satisfiability problem with SCCs, and have a question about topological sorting. The algorithm I'm basing this on is to process SCCs in reverse topological order, which is fine when they're all connected. My algorithm is breaking on cases like this:

3 3
-2 3
1 -2
-2 -1

This makes a graph that looks like this:

There are two sources and two sinks in this graph, and depending on where you start there are multiple topological sorts, so there are two possible final nodes. There are no cycles so each node is an SCC. There are multiple paths from source to sink, so when I do reverse topological order I can either start at sink x3 or sink !x2. The path that will give me a correct answer is to start at !x2, which will result in 1, -2, -3 or -1, -2, -3, both of which are solutions. But if I start at x3, one possible outcome is -1, 2, 3, which is not a solution.

So when I look at my two sinks, how do I decide topologically which is last? Clearly the answer is !x2, but I'm trying to figure out how the algorithm will determine that. I see four possible ideas:

• !x2 is last because it has more nodes leading into it
• !x2 is last because it is at the end of a longer path
• Set the truth value of each of the sinks before I start processing anything
• There is no way to know which is last, so create all possible solutions and test each of them to see if it works.

Or is there something about topologically ordering SCCs I'm not getting here? This is based on the algorithm I used to pass a Strongly Connected Components assignment in an earlier course, so it can't be completely wrong.

Answer 1

Without seeing your code I can't be sure, but my guess is that when you process the literals you're setting a value and then flipping it later when you encounter its negation deeper in the topological order. The key is that once you set a variable, you don't change it again. Skip the literal of any variable that already has a set value.

Edited to add: From your comment I think I see the problem. You mention setting the variable x2 to true when !x2 comes first in the reverse topological sort. You should be setting the literal !x2 to true, which means you set the variable x2 to false. If you do that, then your solver should work not matter which of the sinks you start with.