Cílem projektu je vyřešení 2 grafových problémů s pomocí zvoleného SAT solveru na konkrétních instancích. Jedná se o tyto problémy:
- Vrcholové barvení grafu - Vstupem je neorientovaný neohodnocený graf a přirozené číslo (dále ozn. jako k). Cílem je zjistit, zda je možné každému z vrcholů grafu přiřadit jednu z k barev tak, aby nikdy neměly stejnou barvu vrcholy, které jsou spojeny hranou. Pokud takové přiřazení existuje, má být také nalezeno. Pro zadaný graf je konkrétně cílem zjistit, zda existuje řešení pro k=2 a k=3.
- Nezávislá množina v grafu - Vstupem je neorientovaný neohodnocený graf a přirozené číslo (dále ozn. jako k). Cílem je zjistit, zda je možné v grafu najít množinu k vrcholů takových, že mezi žádnými dvěma vrcholy z těchto k není hrana. Pokud taková množina existuje, má být také nalezena. Pro zadaný graf je konkrétně cílem zjistit, zda existuje řešení pro k=3 a k=4.
|
Požadavky na řešení výše uvedených problémů jsou následující:
- Vytvořte 4 soubory s formulemi odpovídající dvěma problémům se dvěma vstupními čísly, všechny pro stejný zadaný graf.
- Pomocí libovolného SAT solveru zjistěte, zda je formule splnitelná nebo ne a v pozitivním případě si nechejte najít i příslušné ohodnocení.
- Popište myšlenku, na které byly vaše formule založeny tak, aby bylo jasné, jak by se dal obdobným způsobem zakódovat do formule libovolný jiný graf.
- Pokud byla formule splnitelná, znázorněte ve vašem grafu řešení problému odpovídající nalezenému ohodnocení.
|
Všechny grafy mají množinu vrcholů V={A,B,C,D,E,F,G} a množiny hran následující:
- G1: H={(A,B), (A,C), (A,F), (A,G), (B,C), (B,F), (C,F), (E,D), (E,G)}
- G2: H={(A,B), (A,C), (A,F), (A,G), (B,D), (C,E), (C,F), (D,E), (E,G)}
- G3: H={(A,B), (A,D), (A,G), (B,F), (C,D), (C,G), (D,E), (D,F), (E,G)}
- G4: H={(A,G), (B,E), (B,G), (C,E), (C,G), (D,E), (D,G), (E,F), (F,G)}
- G5: H={(A,B), (A,G), (B,C), (B,E), (C,D), (C,G), (D,E), (E,F), (F,G)}
|
|
