Modern techniques for dependency resolution
Just a recap of a short discussion with @haxscramper and @FedericoCeratto on modern dependency resolution.

Nimble found a certain combination of dependencies impossible to resolve even though there is actually a solution.

Modern package managers that handles tens of thousands of packages and/or multiversioning are gradually delegating dependency resolution to SAT solvers as this is a problem that can be modelled as a Satisfiability problem.

Writeups:
- Anaconda, the scientific python distribution which manages 10s of thousands of branches, versions, architectures, optional dependencies: https://www.anaconda.com/blog/understanding-and-improving-condas-performance. Note for personally using for data science, it is still way too slow.
- Mamba, a package manager for conda in C++ that is significantly faster: https://wolfv.medium.com/making-conda-fast-again-4da4debfb3b7

TLDR;
- Both are looking into SAT solver, conda was looking into using Z3 specifically https://github.com/Z3Prover/z3/issues/211.
If we provide Z3, for DrNim nimble can piggyback on it.
- Mamba choose a pragmatic solution `libsolv` from the OpenSuse project which is very package management oriented: https://github.com/openSUSE/libsolv

Note: I think there are other approaches possible from writing that ourselves or using alternative theories like Integer Linear Programming (ILP) but it's more pragmatic to reuse existing blocks that were optimized and stabilized over years of usage here and regarding ILP, I tried to wrap the one for LLVM (http://isl.gforge.inria.fr/) or write one myself (https://github.com/mratsim/hydra) but those are really complex.