I've made some early work on using constraints when I started working on Yarn, but it ended up unpractical because of the sheer execution time it required. A huge number of constraints were required to satisfy the requirements, which was made even worse when you consider that a dependency version might have different sub-dependencies than its other versions.

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.