im trying to figure out why this is trueThe 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 :)
How can you check if a 2SAT problem has a bad loop
complexity theory;logic;satisfiability
The implication graph is constructed using the following ingredients:Vertices: One vertex for each variable, and one for each negation of a variableEdges: For each clause {x,y}, create an edge from -x to y and one edge from -y to xThe 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$bIf b isn't true (i.e. -b is true), then a must be true, which is the implication -b$\to$aIn 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. 