SAT solver can be used to implement xbps-repodb --index, that move packages from stagedata to repodata, ensuring consistency of package requirements.
Real packages, virtual packages and shared libraries are represented as boolean variables. Value of true represents presence of item in repo, false represent absence.