Na zaciatku budem za vybrate povazovat iba tie baliky, ktore pouzivatel prikazal nainstalovat. Pre kazdy vybraty balik PackID a korene jeho grafov zavislosti CondID budem odvodzovat satisfy(CondID,Type,PackID). Tym zabezpecim, aby zavislosti kazdeho vybraneho balika boli zabezpecene. Odvodenie noveho satisfy sposobi prechod prislusnym grafom zavislosti, pricom odvodzovat sa budu atomy doPick(Neg,Op,Name,Ver,Type,PackID) tak, aby nakoniec bol splneny koren prislusneho grafu. Konkretne pre kazdy vrchol sa bud vyberie balik, ktory sposobi splnenie poziadavky prislusneho vrcholu, alebo sa odvodi satisfy pre jeho ALEBO suseda. Ak ma vrchola A suseda, potom sa odvodi satisfy aj pre neho.
Predikat doPick(0,Op,Name,Ver) sposobi, ze pre kazdy balik ktory vyhovuje podmienkam (danym pomocou Op, Name a Ver) sa rozhodne, ci bude alebo nebude zahrnuty do vyslednej konfiguracie. Kedze takyto balik by nemusel existovat ani jeden (a treba zabezpecit aby v kazdom stabilnom modely bol aspon jeden balik vybraty), pouzil som constraint ktory zabezpeci, ze pre kazdy doPick existuje aspon jeden vybraty balik, ktory mu vyhovuje (toto kontroluje predikat doPickSucc). Pre kazdy takto vybrany balik sa zaroven poznaci v akom poradi vzhladom na balik PackID ma byt nainstalovany (pred nim, po nom alebo na poradi nezalezi). Tato skutocnost sa zapamata odvodenim predikatu after. Dalej treba osetrit aby sa do stabilneho modelu nedostali baliky, ktore nie su opravnene (teda konfiguracia by fungovala aj bez nich). Od programu pozadujem aby vypisal jednu najlepsiu konfiguraciu (nie vsetky), preto mozem pouzit weak constraint na pocet vybratych balikov.
Predikat doPick(1,Op,Name,Ver) musi zabezpecit, aby sa ziadny balik, ktory vyhovuje podmienkam nedostal do konfiguracie. To dosiahnem prislusnymi constraintami.
Najprv prejdem vsetky grafy zavislosti nainstalovanych balikov a skontrolujem, ci odstranenim pouzivatelom pozadovanych balikov nedojde k poruseniu niektorych zavislosti (sposob prechodu je rovnaky ako pri druhom prechode). Pre vsetky baliky s takto porusenymi zavislostami odvodim, ze ich odstranenie je vynutene (predikat forceRemove).
Odteraz budem za odstranene povazovat baliky, ktore pouzivatel prikazal odstranit alebo ktorych odstranenie bolo vynutene. Zo zvysnych zakazem odstranit tie, ktore pouzivatel pozaduje (a nie su nutene odstranene). Pre ostatne baliky necham solver urcit, ktore budu odstranene a ktore ponechane. Pomocou weak constraintu zabezpecim, aby boli odstranene vsetky baliky, ktore je mozne odstranit. Potom overim, ci vybrana konfiguracia splna zavislosti vsetkych ponechanych balikov.
Pre kazdy ponechany balik budem odvodzovat satisfyVert pre tie vrcholy z jeho grafov zavislosti, ktore je nutne splnit. Ak vrchol, ktory treba splnit, ma A nasledovnika, potom treba splnit aj jeho. Ak ma ALEBO nasledovnika, potom ho treba splnit iba v pripade, ze nie je splnena podmienka v tomto vrchole. Pre kazdu podmienku v grafoch zavislosti sa da jednoducho odvodit, ci je splnena alebo nie (toto koduje predikat satisfiedCond).