Domáca úloha č.1
Nech G je graf na n vrcholoch. Dominujúca množina je taká množina X vrcholov G, že každý vrchol je buď v X, alebo má suseda v X. Naprogramujte funckiu, ktorá overí, či má graf dominujúcu množinu obsahujúcu najviac n/4 vrcholov. V jazyku C++ naprogramujte tri funkcie:
-
bool dominates4trivial(std::vector<std::vector<int>> graph)
. Táto funkcia má obsahovať jednoduchý (neefektívny) algoritmus na riešenie problému.
-
std::vector<std::vector<int>> dominates4toCNF(std::vector<std::vector<int>> graph)
. Problém preveďte na problém splniteľnosti konjunktívnej normálnej formy.
-
bool dominates4sat(std::vector<std::vector<int>> graph)
. Problém vyriešte pomocou SAT solvera. Ako SAT solver použite togasat.
Graf je reprezentovaný nasledovne. Graf má graph.size()
vrcholov, ktoré sú označené číslami od 0
po graph.size()-1
. Hrana medzi vrcholmi i
a j
existuje práve vtedy, keď graph[i]
obsahuje j
a graph[j]
obsahuje i
. Vektory, ktoré graph
obsahuje neobsahujú žiadne prvky navyše.
Konjunktívnu normálnu formu reprezentujte ako vektor kláuz, pričom klauzy reprezentujte tak, ako to robí togasat.
Okrem správnosti riešenia bude udelený počet bodov závisieť najmä od dĺžky konjunktívnej normálnej formy vygenerovanej dominates4toCNF
.
Dajte si pozor na to, aby vaša funkcia na generovanie konjunktívnej normálnej formy zvládla spracovať aj grafy majúce napr. sto vrcholov (nevadí ak ich SAT solver nebude zvládať spracovať v rozumnom čase). Všimnite si, že triviálny spôsob overenia "najviac n/4 vrcholov" obsahuje (n nad n/4) kláuz, čo je veľa. V komentári stručne vysvetlite na čom je vaše riešenie založené.
Riešenie odovzdajte do 1.12. vrátane (v SEČ) majlom na adresu lukotka.pts@gmail.com.
Všetky funkcie odovzdajte v jednom súbore, nazvanom dominates4.hpp
. Tento súbor nemá obsahovať funkciu main
.
Upozorňujem, neposielajte teraz ani v budúcnosti na túto adresu nič iné ako samotné odovzdanie riešenia domácich úloh (na túto adresu sa prihlasujem iba keď sťahujem domáce úlohy a posielam feedback a aj teraz som tam objavil nejaké majly o bakalárkach).
Bonusové rozšírenie domácej úlohy (maximum s bonusom je 13b miesto 10b)
Bez ohľadu na to, ktorý spôsob riešenia použijete, je vysoko pravdepodobné, že vaša konjunktívna normálna forma má nasledujúcu vlastnosť. Ak existuje jedno ohodnotenie, kde je formula splnená, existuje ich veľmi veľa. Naprogramujte funkcie
std::vector<std::vector<int>> dominates4toCNF2(std::vector<std::vector<int>> graph)
a bool dominates4sat2(std::vector<std::vector<int>> graph)
, kde upravíte konjunktívnu normálnu formu tak, aby výsledná formula spomínanú vlastnosť nemala. Táto úprava môže miesre zväčšiť výslednú formulu, nemalo by to všat byť zásadné zväčšenie. Porovnajte fungovanie prvého a druhého prístupu. V komentári stručne vysvetlite, váš postup a zhrňte výsledky porovnania.