Addendum dated 12 December 2017: Bulatov and Zhuk have shated the best paper awards at FOCS 2017 with Ola Svensson and Jakub Tarnawski. See here. Thanks to Lance Fortnow for sharing this piece of news with me.
Status of the three proposed proofs for the Dichotomy Conjecture
As several people in the community have been aware of, the proof of Feder, Kinne and Rafiey has been suspect since it appeared. The parts where they are unclear, or wave hands over details, are precisely the parts where, in the opinion of several experts, the main difficulty was. Unfortunately, this has led to a counterexample and the retraction by Feder, Kinne and Rafiey of the claim they have solved the Dichotomy Conjecture. Their retraction can be found in the comments which replace the abstract of the fourth and most current version of their paper, see https://arxiv.org/abs/1701.
More concretely, it was pointed out in private conversation of several experts that their proof fails on Miklós Maróti's ‘tree-on-Mal’cev’ kind of problems, when they are eliminating what they call `non-minority cases'.
Incidentally, ‘tree-on-Mal’cev’ is not some obscure class of CSPs. As people who are reading it will surely agree, generalizing Maroti's result to 'semilattice-on-Mal’cev’ is the cornerstone of Andrei Bulatov's proof of the Dichotomy Conjecture, the rest is a (very technical and difficult) generalization of the ideas which solve this special case. Even though Feder, Kinne and Rafiey were working only on digraph templates, while ‘tree-on-Mal’cev’ does not specify the relations, just the polymorphisms, the construction by Bulin, Delić, Jackson and Niven, which improves on the original one by Feder and Vardi, reduces a general template to a digraph one, while preserving not only the complexity but also most polymorphisms. So Feder, Kinne and Rafiey's algorithm should have been able to solve those ‘tree-on-Mal’cev’ templates.
Ross Willard, who also was among the experts involved in the initial conversation in January, took the trouble to actually construct digraph CSPs out of the 'tree-on-Mal'cev' CSPs. He constructed out of a tree-on-Mal’cev template a digraph template which contradicts the claim in Feder, Kinne and Rafiey paper that certain situation in the digraphs allows the domain of a variable, and thus the multi-sorted instance, to be reduced by a vertex. This contradicts the whole philosophy of their approach, creating a barrier where they can't proceed with reductions. He emailed the authors of Feder/Kinne/Rafiey his counterexample and, working together, they simultaneously published the retraction, while he published his counterexample on arxiv. The counterexample is available at https://arxiv.org/abs/1707.
On the flip side, at a fairly large conference in June in Novi Sad, Serbia, both Bulatov and Dmitriy Zhuk had plenary talks. After the afternoon in which they exposed their proofs of the Dichotomy Conjecture to a general audience, a special event was organized which lasted almost three hours. The idea was that each would discuss minutiae of their proofs and answer challenges from present experts. In the audience there were about a dozen people who may safely be called experts on the algebraic approach to CSP and most have read in detail large parts of both proofs. There were many interruptions and serious questions were asked, but both proofs survived all challenges unscathed. My degree of confidence after this event in both Bulatov's and Zhuk's proofs is very high, well over 90%, and the odds that both are wrong are really small.
Overview of the proofs by Bulatov and Zhuk
The proof by Bulatov has several ingredients:
1. his own colored graph theory of algebras which he has been developing for the past decade or so and which he additionally improved on for this paper,
2. a new centralizer notion which is similar to the classical one from 1980’s Freese and McKenzie book, but this one involves binary polynomials instead of terms of arbitrary arity,
3. a connectedness notion, dubbed ‘coherent sets’, between domains of various variables, somewhat reminiscent of what McKenzie and I called ‘strands’ in an unpublished paper about semilattice-over-Mal’cev CSPs, but much more complicated
4. Maróti’s reduction which solves one of his reduced cases. This reduction uses polynomials of the polymorphism algebra (operations created from polymorphisms by fixing some variables as constants) to find a related smaller CSP instance, which either has no solution, in which case the original one doesn’t have a solution, or has a solution, in which case that solution shows how to reduce the original instance to a smaller one,
5. a crazy amount of consistency which assures that another of his three reduced cases must have a solution if it is nonempty,
6. the old few subpowers algorithm in his third reduced case, and finally
7. a massive induction which lowers the location of congruence covers modulo which coherent sets are considered, working simultaneously through various congruence lattices of variable domains. When they can appear only at the bottom then the reduced cases 4., 5. and 6. occur. It is this last part which is the hardest and requires most scrutiny. The rest is mostly clear to experts (personally, I would say I am sure the rest is correct).
I understand Zhuk’s proof much less, but the main ingredient is his structure theory of relations. He subjects the constraint relations to several extreme conditions he invented (and can assume after some effort). Next, he also works down the congruence lattices of various domains of variables. There are three types of reductions he uses to reduce to an instance which satisfies all these assumptions. When the congruences have also been subjected to extreme assumptions, then his theory of relations claims that each lower cover of the current congruence in each domain of variable is a Mal’cev cover. He can solve the Mal’cev problem, which is pretty much a system of linear equations, and arrive at the solution space to the factor problem. Also, he can test whether this is the same space as the space of all solutions to the initial instance, factored. This is easy, he just selects one solution of the factored problem and uses its classes as new domains of variables. They are smaller than the original ones so inductively he can solve it. If it has a solution, he found a solution to the original instance. If not, he works on finding a new constraint which does not affect the solution space to the original instance, but reduces the dimension of the solution space to the factor problem. (Finding this constraint relies on his structure theory and on other reductions, and is probably the hardest part of his proof.)
There is a circular nature to Zhuk’s proof which uses all four types of reductions in previous cases to prove the one he is currently applying. This is an idea similar to ‘simultaneous induction’ in Adian and Novikov’s proof of Burnside conjecture which was later much used in group theory.
The very high-level bird-eye view is that Bulatov reduces everything to consistency checking or few subpowers (when there are no ‘semilattice edges’), Zhuk reduces in a circular way, but Mal’cev is what he seems to end at, while Feder, Kinne and Rafiey also reduce everything to Mal’cev, but have a problem in eliminating some semilattice covers. Since the absence of semilattice covers is the same as having few subpowers, the missing part in Feder, Kinne and Rafiey is serious.