Detail práce
Knihovna pro binární rozhodovací diagramy
Efektivní manipulace Booleovských funkcí je důležitou součástí mnoha počítačových návrhů. Jako datová struktura pro reprezentaci a manipulaci s Booleovskými funkcemi se běžně používají binární rozhodovací diagramy. Tyto diagramy se běžně používají v mnoha odvětvích, jako je například ověřování modelů, verifikace systému, návrh obvodů apod. V této práci jsou popsány tyto diagramy a jsou zde uvedeny i jejich modifikace. Dále jsou v této práci uvedeny a popsány techniky pro efektivní manipulaci a reprezentaci binárních rozhodovacích diagramů. Mimoto tato práce popisuje návrh a implementaci knihovny, která bude s těmito diagramy pracovat. Na závěr je tato knihovna porovnána s dobře známou a silně optimalizovanou knihovnou CUDD, která je volně dostupná. Výsledky ukázaly, že navrhovaná knihovna je poměrně blízká CUDD (ve většině případů o něco rychlejší)
Booleovské funkce, symbolická manipulace, binární rozhodovací diagramy.
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Oponent hodnotil práci stupněm 4F, protože svým rozsahem a obsahem nesplnila nároky kladené na diplomovou práci. Student nedokázal vyvrátit výtky oponenta. Komise shledala nedostatky práce natolik závažné, že se práci rozhodla hodnotit jako nevyhovující.
- Proveďte znovu váš srovnávací experiment se zapojením garbage collectingu, který odpovídá koncepci knihovny CUDD. Interpretujte výsledek.
- Zdůvodněte paměťové nároky výpočtu.
Bartík Vladimír, Ing., Ph.D. (UIFS FIT VUT), člen
Bidlo Michal, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Hrubý Martin, Ing., Ph.D. (UITS FIT VUT), člen
Meduna Alexander, prof. RNDr., CSc. (UIFS FIT VUT), člen
Steingartner William, Ing., Ph.D. (TUKE), člen
@mastersthesis{FITMT17839,
author = "Petr Jank\r{u}",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Knihovna pro bin\'{a}rn\'{i} rozhodovac\'{i} diagramy",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2015,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/17839/"
}