How can you check if a 2SAT problem has a bad loop

Question

im trying to figure out why this is true

The clauses {a,b}, {b,~c}, {c,~a} constitute a 2SAT problem with an implication graph without bad loops.

Can someone show me how to illustrate this and indicate how i can find wether any 2SAT problem has a bad loop or not, Thank you so much :)

Answer 1

The implication graph is constructed using the following ingredients:

• Vertices: One vertex for each variable, and one for each negation of a variable
• Edges: For each clause {x,y}, create an edge from -x to y and one edge from -y to x

The following should be the implication graph corresponding to your set of clauses:

A bad loop (I'm guessing this is what you want, haven't encountered that wording before) is a loop in the implication graph that contains both a variable and its negation (i.e. both x and -x). Clearly there is no such loop in your case.

Why "bad loop"? It is because each edge represents an implication that necessarily must hold for your 2-SAT instance. For example, the first clause reads "a or b". If this clause is to be satisfied, then we must have one of the two variables true. So:

• If a isn't true (i.e. -a is true), then b must be true, which is the implication -a$\to$b
• If b isn't true (i.e. -b is true), then a must be true, which is the implication -b$\to$a

In a "bad cycle", you have a cycle of such implications, so that x$\to$...$\to$-x$\to$...$\to$x. Such a cycle of implications can never be satisfied, otherwise x would be both true and false at the same time. So if you have any bad cycles, the 2-SAT formula is unsatisfiable!

In fact, a 2-SAT formula is unsatisfiable when, and only when, there is a bad cycle in the implication graph. So your formula is, by the absence of bad loops, satisfiable. The proof of satisfiability in the case of no bad loops even yields a poly-time algorithm to find a satisfying assignment (which is great : ) )

So how to assign values to the variables and satisfy your (or any) 2-SAT formula? I'll refer to https://en.wikipedia.org/wiki/2-satisfiability#Strongly_connected_components for the algorithm, but be warned that you need to know of the concept of "strongly connected component" to fully understand the algorithm.