First break into SCC's. Each SCC represents equivalence: since there is a
path from every variable to every other variable, they must take on the
exact same value. Hence if and are in the same SCC, we don't
have a solution, because this means that
Let's say we find SCC's where this does not happen. Now, zoom out and think of
the condensation DAG. We want to assign true/false to each node in the SCC DAG.
How should we assign true/false? Say that and are in two
different components. So this means that we have the possible orderings
Hence, if implies , we should set to . The other
assignment is inconsistent .
- : (Inconsistent!)
- : (Consistent, principle of explosion)