An extremely formal week

The Oct 16 - Oct 22 week started with Codeforces Round 441 on Monday (problems, results, top 5 on the left, analysis). fateice demonstrated impressive speed in solving 6 problems in 50 minutes only, good 20 minutes earlier than everybody else. Congratulations on the victory!

The problem F in this round was quite nice: you are given a bipartite graph with at most 200000 vertices each each part. Each vertex in the left part has exactly two edges to different vertices in the right part. Each vertex in the left part also has a weight. You need to find the weight of the maximum weight matching in this graph (but you don't need to output the matching itself). Of course, the standard maximum matching algorithms would be quadratic or at least O(n*sqrt(n)) and thus too slow for this problem. How to solve it faster?

On Sunday, the onsite portion of TopCoder Open 2017 started with its Semifinal 1 (problems, results on the left). xudyh solved the medium problem in 25 minutes, while everybody else could not solve it at all — what a commanding performance! scott_wu and rng_58 also advanced to the finals thanks to fast times on the easy problem.

In my previous summary, I have mentioned an Open Cup problem about formal proofs (problem H here): you are given an undirected connected graph with at most 73 vertices and 492 edges, and a desired parity for each vertex (either odd, denoted by 1, or even, denoted by 0). The sum of all parities is 1 modulo 2. You need to prove that there doesn't exist a subset of edges of the graph with the desired parity of the number of edges adjacent to each vertex. It would be easy to prove, as it is well known that the number of vertices of odd degree in any graph is always even. However, you're only interested in proofs stated in a specific form.

Such proof is a sequence of clauses. Each clause is an "or" of zero or more variables and/or their negations. Each variable corresponds to an edge in the graph, and is true if we take this edge, and false otherwise. Each clause must be built in one of the three ways:

1. In can be an axiom, which in our case means that it must contain the variables corresponding to all edges adjacent to some vertex of the graph, with the number of negated variables having the parity that is opposite to the desired parity for this vertex. For example, consider a vertex of degree 5 and desired parity 0, with adjacent edges a, b, c, d, e. A valid axiom for this vertex would be for example !a|!b|c|d|!e, which would be false only if variables a,b,e are true, and variables c,d are false, but that would mean that the vertex has 3 adjacent edges which doesn't satisfy its parity requirement, so this axiom is always true.
2. It can be a conclusion, in which we take two previous clauses of form A|x and B|!x, and make a new clause A|B. Since both original clauses are true the conclusion is true as well.
3. It can be a transformation of a previous clause. We take a previous clause and a permutation of the set of all variables and their negations, and apply the permutation to the elements of the clause to get the new clause. The permutation can not be arbitrary: it must be an automorphism of the set of axioms (map every axiom to an axiom). Note that transformations are not a strictly necessary operation, as we could have constructed the resulting clause by applying the automorphism to the axioms used to build the original clause, and then repeating how it was built, but it allows to dramatically reduce the number of clauses in a proof.

Your goal to derive an empty clause in at most 1000 steps, which would mean a contradiction, and prove that the parities goal is impossible to achieve.

First, let's solve our problem for the case where our graph is a tree. We will apply a recursive procedure that takes a subtree, and builds a clause with just one variable corresponding to the edge going into that subtree, either negated or not. For a leaf, such clause is just an axiom. For an internal vertex, we can recursively build such clauses for edges going to its children, and then build an axiom from negations of those clauses, and choosing whether to negate the edge to the parent to obtain the required parity for the axiom. We can then eliminate all variables but one from this axiom using the conclusion, as we have negated single variables for all edges going to the children.

When we reach the root of the tree, we apply the same procedure, only there's no extra variable for the edge to the parent. The condition on the sum of all parities will guarantee that the above approach is still applicable, i.e. the axiom we need to cancel out all variables will be a valid axiom for the root (a formal proof of that fact would probably inductively find that the edge going from a subtree gives us a negated or non-negated clause based on the sum of parities in that subtree). And we will obtain an empty clause after eliminating all variables in the root, thus completing the required formal proof in less than 2n steps, where n is the number of vertices.

Now how to adapt this approach for the case where the graph is not a tree? Let's pick an arbitrary spanning tree in it, and apply the same idea. Whenever we need to create a new axiom for a vertex, let's keep all variables corresponding to the edges that are not in the spanning tree non-negated. This does not affect the validity of axioms since it depends only on the number of negated variables. In the end, instead of an empty clause we will get a clause that is an or of all edges that are not in the spanning tree, and does not have variables corresponding to the edges of the spanning tree.

This is where the third operation type, the transformation, comes into play. For each edge not in the spanning tree consider its fundamental cycle formed by this edge and the path between its ends in the spanning tree. Let's apply a transformation that negates all variables corresponding to this cycle. This is a valid transformation since for each vertex it negates 0 or 2 variables, which does not affect the parity, and thus maps axioms to axioms. In our clause it will negate exactly one variable, since we don't have variables corresponding to the edges of the spanning tree, and we can then use conclusion to remove that variable from our clause. We can then repeat this process for all edges not in the spanning tree and obtain the empty clause in 2(m-n+1) additional operations, or less than 2(m+1) overall, where m is the number of edges, which is good enough.

Thanks for reading, and check back soon!