Cílem projektu je vyřešení 3 grafových problémů s pomocí zvoleného SAT solveru. Základem jsou následující 3 problémy, po dohodě s vyučujícím si může student 1-2 problémy změnit za jiné.
- 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.
- 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.
- Hamiltonovská kružnice v grafu - Vstupem je neorientovaný neohodnocený graf. Cílem je zjistit, zda je v grafu existuje uzavřená cesta (tzv. kružnice), která prochází každý vrchol grafu právě jednou (tzn. je Hamiltonovská). Pokud taková kružnice existuje, má být také nalezena.
|
Požadavky na řešení výše uvedených problémů jsou následující:
- V libovolném jazyce vytvořit program, který načte graf ze souboru, další informace získá (např. číslo k, když je pro problém potřeba) buď dotazem od uživatele nebo jako parametr příkazové řádky, vytvoří přislušnou formuli, zavolá nějaký SAT solver a odpověď SAT solveru interpretuje uživateli ve srozumitelné podobě (např. pro každou z k barev vypíše seznam vrcholů, které jsou touto barvou obarveny apod.).
- Není vyžadováno GUI, stačí konzolová aplikace.
- Může jit o jeden program řešící (na základě parametrů příkazové řádky, volby uživatele, ...) všechny 3 problémy nebo o 3 samostatné programy.
- Použitý SAT solver může být libovolný, ať už zmíněný na cvičeních (MiniSAT, Sat4J,...) nebo jiný. Může být volán jako externí program, nebo použitý ve formě knihovny. Nesmí být ale využity vlastnosti některých SAT solverů, kde je možné problém popsat nějakým speciálním jazykem a tato specifikace je do formule převedená automaticky.
- Grafy budou zadány v souborech s jednodnou syntaxí pro všechny problémy i studenty. Soubor je textový, ne binární. Na prvním řádku je kladné číslo znamenající počet vrcholů grafu (např. pro číslo 5 to chápeme tak, že graf má vrcholy pojmenované 1,2,3,4,5). Každý další řádek obsahuje dvě, mezerou oddělená, přirozená čísla ne vyšší než počet vrcholů. Pokud jsou nenulová, reprezentují hranu mezi příslušnými dvěma vrcholy. Řádkem s dvojicí "0 0" popis grafu končí (tato dvojice je jen jako zarážka, sama nereprezentuje hranu), cokoliv za tímto řádkem je bráno jako komentář a bude programem ignorováno. Není nutné řešit situace, kdy by vstupní soubor neodpovídal této specifikaci.
|
Součástí projektu je text popisující řešení, obsahující:
- Jméno, příjmení a login studenta
- Stručný popis řešených problémů (pokud jsou to ty tři uvedené výše, tak stačí jejich jména)
- Pro každý problém popsáno, jak se instance (tedy konkrétní uživatelem dodané zadání) zakóduje do formule a jak se z nalezeného ohodnocení dekóduje řešení v grafových pojmech.
- Jaký SAT solver byl použitý a jak (jako externí program nebo jako knihovna).
- Jak výsledný program přeložit (překladač, příslušné volby při překladu) a jak ho spustit (parametry příkazové řádky apod.). Pro překlad je lepší dodat Makefile nebo kompletní projekt vývojového prostředí (CodeBlocks, Visual Studio, ...) - pak není nutné popisovat překlad, ale zmínit to vývojové prostředí včetně verze.
|
|
