0
$\begingroup$

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 :)

$\endgroup$
3
$\begingroup$

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:

enter image description here

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.