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. Dále je diskutována potenciální aplikace vyvinuté knihovny v knihovně VATA pro manipulaci se stromovými automaty. Na závěr je tato knihovna porovnána s dobře známou a silně optimalizovanou knihovnou CUDD, která je volně dostupná a s knihovnou CacBDD. Výsledky experimentů ukázaly, že navrhovaná knihovna je poměrně blízká CUDD a CacBDD (dosahuje srovnatelného a většinou i lehce lepšího výkonu).
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. Student následně odpověděl na otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm "C".
Kreslíková Jitka, doc. RNDr., CSc. (UIFS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Růžička Richard, doc. Ing., Ph.D., MBA (UPSY FIT VUT), člen
Šlapal Josef, prof. RNDr., CSc. (UM OADM FSI VUT), člen
Zbořil František, doc. Ing., Ph.D. (UITS FIT VUT), člen
@mastersthesis{FITMT18227,
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/18227/"
}