Explosion

Problem Name: Explosion
UVa ID: 11861
LightOJ ID: 1407
Keywords: 2sat, graph, strongly connected components, backtracking

This is an interesting 2-SAT problem. As most 2-satisfiability problems, it can be solved using a graph that represents the corresponding CNF formula, and working on its strongly connected components.

However, the interesting part comes in the “council opinions” given in the input, which represent constraints with 3 variables. Since \(k\) is at most 5, a little bit of brute force should work.

I tried this at first, and wrote a brute force solution that tried all \(3^k\) options (reconstructing the S.C.C.s for each alternative) and, of course, it was very slow…

What is required is a little bit of pruning. This is where the “back-tracking” part comes up. If \(k=0\), then running the standard 2SAT algorithm one time is sufficient. But if \(k > 0\), you can start by checking the 2SAT on the original graph (without any council options), and if its value is false (can’t be satisfied), then you can give your answer and you’re finished. Otherwise, start testing with all options from the first council member, and only go deeper in the tree of options if the 2SAT algorithm up to that point returns true.

The idea is to add constraints from the council members one at a time, and if at some point the 2SAT graph can’t be satisfied, then it’s not necessary to go through any of the remaining council members for that branch.

This reduces the number of steps drastically, and is enough for an AC.