| Meno: | Matúš |
|---|---|
| Priezvisko: | Kukan |
| Názov: | Využitie SAT-solverov pri riešení ťažkých úloh |
| Vedúci: | Mgr. Richard Štefanec |
| Rok: | 2011 |
| Kľúčové slová: | SAT-solver, redukcia na SAT, NP-úplný problém |
| Abstrakt: | Vývoj najmodernejších SAT-solverov v posledných rokoch výrazne pokročil. V práci sa zaoberáme možnosťami využitia heuristík a technológií, ktoré sú v nich implementované a neustále zdokonaľované, na rýchle riešenie niektorých NP-úplných grafových problémov. Na dosiahnutie cieľa sa snažíme nájsť čo najvhodnejšie zakódovanie vstupného grafového problému do inštancie SATu. Zároveň jednotlivé kódovania porovnávame aj vzájomne a aj s backtrackovým algoritmom. |
Súbory bakalárskej práce:
| SAT-solvery.pdf |