It was not mentioned in the post that dnf is based on the openSUSE dependency SAT solver (libsolv) that was created by Michael Schroeder years ago and that powers libzypp and zypper since openSUSE 11.0.
The dnf developers built a thin layer on top of it, called hawkey, and then build dnf in python on top of hawkey.
One of the biggest innovations of libsolv is not only the SAT based solver but also the .solv format which allows to store package metadata for big amounts of packages in an efficient way and operate the solver directly on it.
It was not mentioned in the post that dnf is based on the openSUSE dependency SAT solver (libsolv) that was created by Michael Schroeder years ago and that powers libzypp and zypper since openSUSE 11.0.
The dnf developers built a thin layer on top of it, called hawkey, and then build dnf in python on top of hawkey.
One of the biggest innovations of libsolv is not only the SAT based solver but also the .solv format which allows to store package metadata for big amounts of packages in an efficient way and operate the solver directly on it.
https://github.com/openSUSE/libsolv