Detail práce
Využití SAT solverů v úloze optimalizace kombinačních obvodů
Tato práce zavádí využití řešení problému SAT a jeho modifikací v úloze evolučního návrhu kombinačních obvodů. Motivací využití těchto problémů je zrychlení ohodnocování chromozomů kandidátních řešení fitness funkcí během evoluce v případech, kdy selhává metoda klasické simulace. Využití problému SAT, respektive #SAT umožňuje oproti simulaci zrychlení zejména pro komplikované obvody s velkým počtem vstupů. Implementované řešení se zalkádá právě na problému #SAT. Celkem byly implemenyovány dvě různé varianty využití tohoto problému. Varianty se liší metodou kontorly rozdílných hodnot na výstupech obvodu. Protože implementované řešení využívá k reprezentaci obvodu logickou formuli a zkoumá její splnitelnost, časová složitost algoritmu závisí především na logické složitosti navrhovaného obvodu.
Evoluce, evoluční návrh hardwaru, hardware, HW, SAT, splnitelnost, kombinační obvod,návrh kombinačních obvodů, genetické programování, logika, umělá inteligence, AI.
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 oponenta a na další 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 "B".
- Jaký by byl přínos inkrementálního režimu SharpSAT solveru oproti verzi, kde se všechny výstupy kontrolují najednou?
- Jaké SAT solvery je možné ve vaší implementaci použít?
Jaroš Jiří, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Martínek Tomáš, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Vašíček Zdeněk, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT), člen
Vranić Valentino, doc. Ing., Ph.D. (FIIT STU), člen
@mastersthesis{FITMT13810,
author = "Vojt\v{e}ch Mina\v{r}\'{i}k",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Vyu\v{z}it\'{i} SAT solver\r{u} v \'{u}loze optimalizace kombina\v{c}n\'{i}ch obvod\r{u}",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2019,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/13810/"
}