That being said, I'm not an expert in SAT logic, and it's quite possible a better solution is possible! Maybe some kind of hybrid algorithm, possibly? In fact, one thing I'd really like to do in medium term would be to externalize the resolver part of Yarn - this way, it would be much easier to experiment with it to try to find algorithms that fits various requirements. If you want correctness you would use a slow but comprehensive algorithm, if you want speed you would use a naive algorithm like the one in the article, etc.
Now that I think about it, it's quite possible that the process was apparently hanging on the same issue I describe in my article, where babel-core depends and babel-cli and vice versa. Maybe it would work better if I were to run the process a first time with a simple algorithm like the one exposed in the article, that would clear up any dependency loop, then a second more complex pass that wouldn't have to deal with this.