Author here. I glossed over this in the article, but the solver is actually privileging higher versions as you suggest. In the "set" step, when we arbitrarily set a variable to true, we have a heuristic that picks the highest possible version of the package.