Does anyone know how Linux system package managers solve this problem, SAT or something more? It's also more difficult problem because of having to maintain ABI compatibility.
RPM based distributions typically use dnf, which uses the SAT solver library libsolv https://github.com/openSUSE/libsolv.
I'm not 100% sure if this is current, but APT uses (or used) a heuristics search, but it is possible to configure it to use an external solver instead. See https://salsa.debian.org/apt-team/apt/-/blob/main/doc/extern...