A 2-SAT week

The contests of July 31 - Aug 6 week started with the second competition day of IOI 2017 on Tuesday (problems, overall results, top 5 on the left). As expected, only the three highest scorers of day 1 had a real chance for the first place, and Yuta Takaya has grabbed this chance with the amazing score of 300 out of 300. Well done!

On Saturday, my fruitless attempts to qualify for the TopCoder Open onsite in Buffalo started with TopCoder Open 2017 Round 3A (problems, results, top 5 on the left, analysis). tourist has claimed the first place thanks to solving both the easy and the hard problem - congratulations - but qualification was also possible with easy+challenges, as Scott and Igor have demonstrated.

I could not figure out the solution for the hard problem in time, even though I suspected it would involve a reduction to 2-SAT from the very beginning. Can you see the way?

You were given a tree with n<=250 vertices and need solve a system of at most 250 equations on this tree with m<=250 variables x₁, x₂, ..., x_m , where each variable must correspond to some vertex in the tree. Several variables can correspond to the same vertex. Each equation has the following form: in the path from vertex x_ai to vertex x_bi the vertex closest to vertex p_i must be the vertex q_i.

Somewhat orthogonally to this particular problem, I felt like my general skill of reduction to 2-SAT could use some improvement. It seems that there are some common tricks that allow to replace complex conditions with just "or"s of two variables. For example, suppose we want a constraint "at most one of this subset of variables is true". It could naively be translated into n² 2-SAT clauses. However, we can introduce auxiliary variables to get by with only O(n) clauses: "b_i must be true when at least one of the first i original variables a_i is true" with clauses b_i->b_i+1 and a_i->b_i. Disallowing two true variables is then done via the clause b_i->!a_i+1.

What are the other cool 2-SAT reduction tricks?

Thanks for reading, and check back as I continue to remember August and September :)