JOIN
Get Time
forums   
Search | Watch Thread  |  My Post History  |  My Watches  |  User Settings
View: Flat (newest first)  | Threaded  | Tree
Previous Thread  |  Next Thread
2sat examples to train with | Reply
Hello

I would like to practise some 2-sat(isfiability) problems. Are there any good explanations and/or practise problems available on this subject?

Thanks
Re: 2sat examples to train with (response to post by Shazan) | Reply
TORNJEVI (POI).
SUPSUP (SPOJ).
Piece it Together (NWERC 2011).
Idol (NWERC 2012).

You can find more using an online judge problem classifier.
Re: 2sat examples to train with (response to post by hex539) | Reply
I've attended NWERC 2012 and didn't solve Idol. I would like some explanation on the subject first, to get an idea of the theory. Is there any (good) explanation regarding 2sat problems, e.g. with an example? Googling 2-sat provides loads of sheets from universities and the theory behind it, yet not any explanation nor example.
Re: 2sat examples to train with (response to post by Shazan) | Reply
There are 3 algorithms described on Wikipedia.

When I was undergrad, I came up with a solution using strongly connected components. The crucial observation is that (x or y) is equivalent to (not x -> y) and (not y -> x). Now you have a graph containing x, (not x) for all variables x and implications can be viewed as oriented edges - this is called implication graph.

Implication is transitive, so x -> y and y -> z implies x -> z. This is the same as doing two steps in the implication graph.

If you have both (x -> not x) and (not x -> x), you have a contradiction. So you need to check if x and (not x) lie in the same strongly connected component in the implication graph. This can be done in linear time.

Finding a satisfying assignment is a bit more tricky, but can be done once you have the strongly connected components.
Re: 2sat examples to train with (response to post by lukasP) | Reply
Hmmm I see. So if you can go from x to not(x) somehow in a few steps in the directed graph, you have a contradiction therefore the problem cannot be satisfied?
Re: 2sat examples to train with (response to post by Shazan) | Reply
Yes.

(x -> not x) and (not x -> x) is saying "x is true if and only if x is false".
Re: 2sat examples to train with (response to post by Shazan) | Reply
The Ministers' Major Mess (WF 09)
RSS