I have received the following contribution by Petar Marković, who summarizes recent developments related to the three proofs of the Dichotomy Conjecture that have been proposed since the start of the year and provides an overview of the proofs by Bulatov and Zhuk. The first part of the post is based on a comment Petar posted here. The second is more technical and provides an overview of the proofs by Bulatov and Zhuk, which will be presented at FOCS 2017. I hope that Petar's overview will entice some experts who have not read those proofs to do so and will help them as they delve into the technicalities. Thanks to Petar for taking the time to summarize his understanding of the proofs with the community.
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.02409.
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.09440.
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.
