On internals I was informed about the great blog post introducing PubGrub.

We have an ad hoc implementation of most of the conflict clause parts. The learning parts are questionable do to the "sudoku" problem, it is often faster to prove something is wrong by trying it then by rigorous argument.

But PubGrub uses its data structures to report much more in its error messages. Getting grate error messages that are inspired by are best competition is one of rusts great strengths.
We should get our error messages to be as good as PubGrub's, if we need to by using their algorithm (as the blog post suggested.)