|
|
Plánovací algoritmy a simulace plánu v logistické doméně
Štefan, Zdeněk ; Toropila, Daniel (vedoucí práce) ; Valla, Tomáš (oponent)
Bakalářská práce se zabývá porovnáním některých technik pro řešení plánování v logistické doméně. Její cílem je porovnání schopností těchto technik z umělé inteligence řešit zadaný problém z hlediska optimality nejen mezi sebou, ale i s plány navrženými lidmi. Protože ne všechny plánovače vrací paralelní plány, je potřeba tyto plány paralelizovat. Práce ukazuje, že některé algoritmy dosahují dobré výsledky ve srovnání s lidskými plány, bohužel však kvůli časové a paměťové náročnosti nemůžou být v dnešní době běžně používány pro řešení náročnějších úkolů.
|
|
|
Hledání minimálních splňujících ohodnocení Booleovských formulí
Švancara, Jiří ; Balyo, Tomáš (vedoucí práce) ; Trunda, Otakar (oponent)
V této práci zkoumáme algoritmy a techniky pro řešení Booleovské splnitelnosti. Dále se zabýváme možnostmi jejich použití při řešení weighted short SAT, což je zobecnění problému splnitelnosti. Toto zobecnění požaduje nalézt splňující ohodnocení za použití minimálního součtu vah proměnných. K řešení tohoto problému zavádíme tři pravdivostní ohodnocení proměnných - True, False a Unassign. Ukážeme, že ne všechny algoritmy a techniky používané v moderních SAT solverech můžeme aplikovat v našem programu. Ty, které můžeme, převedeme tak, aby používali námi nadefinované pravdivostní ohodnocení. Různou kombinací takto převedených technik dostaneme několik verzí solveru, které mezi sebou na závěr porovnáme. Powered by TCPDF (www.tcpdf.org)
|
|
|
Strukturované problémy pro SAT
Klátil, Jan ; Hric, Jan (vedoucí práce) ; Kučera, Petr (oponent)
Název práce: Strukturované problémy pro SAT Autor: Jan Klátil Katedra: Katedra teoretické informatiky a matematické logiky Vedoucí bakalářské práce: RNDr. Jan Hric, Katedra teoretické informatiky a ma- tematické logiky Abstrakt: Práce se zabývá implementací generátoru nestrukturovaných dat CSP modelu RB ve formátu XCSP a implementací několika generátorů strukturova- ných dat ve formátu XCSP a DIMACS, za kterými stojí problémy umisťování N-královen, hledání Hamiltonovského cyklu a rozdělování množiny čísel do v sou- čtu stejných podmnožin. Pomocí délek běhů SAT řešiče RSAT pak porovnáváme data získaná pomocí stejného problému přímo ve formátu DIMACS a převede- ním z formátu XCSP. Dalším srovnáním podrobujeme data vynuceně splnitelná a nesplnitelná a spojování dat strukturovaných a nestrukturovaných na úrovni formátu XCSP. Klíčová slova: strukturovaný problém, SAT 1
|
|
|
Polynomiální rovnice nad konečnými tělesy a algebraická kryptoanalýza
Seidl, Jan ; Stanovský, David (vedoucí práce) ; Drápal, Aleš (oponent)
Název práce: Polynomiální rovnice nad konečnými tělesy a algebraická kryptoanalýza Autor: Jan Seidl Katedra: Katedra algebry Vedoucí diplomové práce: doc. RNDr. David Stanovský, Ph.D., Katedra algebry Abstrakt: Předložená práce se zaobírá postupem algebraické kryptoanalýzy, při kterém je nejprve problém prolomení šifry převeden na problém nalezení řešení polynomiální soustavy rovnic a následně je problém nalezení řešení této rovnice převeden na problém SAT. Práce popisuje konkrétně metody, které umožňují převést problém prolomení šifry RC4 na problém SAT. Jed- notlivé metody byly naprogramovány v programovacím jazyce Mathematica a následně aplikovány na RC4 s délkou slova 2, 3. Pro nalezení splnitelného ohodnocení výsledné logické formule byl použit SAT-solver CryptoMiniSAT. V případě RC4 s délkou slova 2 bylo dosaženo nalezení řešení v rozpětí 0,09 až 0,34 sekundy, v případě RC4 s délkou slova 3 pak bylo dosaženo na- lezení řešení v rozpětí 1,10 až 1,23 sekundy. Klíčová slova: RC4, SAT, CryptoMiniSAT 1
|
|
|
Třídy Booleovských formulí s efektivně řešitelným SATem.
Vlček, Václav
Práce se zabývá třídami Booleovských formulí, pro které je problém splnitelnosti (SAT) řešitelný v polynomiálním čase. Zkoumá chování těchto tříd vzhledem k základním operacím s formulemi (komplementaci literálu, komplementaci proměnné, odebrání literálu nebo klauzule, částečné dosazení a spojení formulí). Dále se zabývá problémem rozpoznávání náležení formule do dané třídy, rozpoznávání splnitelnosti dané formule a vzájemnými vztahy těchto tříd vzhledem k inkluzi.
|
|
|
Compilation-based Approaches for Automated Planning
Pantůčková, Kristýna ; Barták, Roman (vedoucí práce) ; Chrpa, Lukáš (oponent)
Jedním z možných přístupů k automatickému plánování je kompilace na problém splnitelnosti (SAT) nebo na splňování omezujících podmínek (CSP). Kompilace nám umožňuje využít vývoje SAT nebo CSP řešičů. V rámci této diplomové práce implementujeme tři z nedávno navržených kódování určených ke kompilaci plánovacích problémů: TCPP, R2 ∃-Step encoding a Reinforced En- coding. Všechny tyto přístupy hledají paralelní plány. Protože se ale liší v definici paralelního kroku a používají jiné proměnné a podmínky, rozhodli jsme se porov- nat jejich výkonnost na plánovacích problémech používaných na mezinárodních plánovacích soutěžích. R2 ∃-Step encoding jsme modifikovali, protože původní verze tohoto kódování nebyla pro naši implementaci vhodná. Naše verze to- hoto kódování používá méně proměnných i podmínek. V této diplomové práci také ukazujeme, jak závisí výkonnost Reinforced Encoding na definici paralelního kroku. Dále uvádíme redundantní podmínky, které mohou být použity k rozšíření těchto kódování. Ačkoliv obecně tyto podmínky nebyly užitečné, dokázaly mírně zlepšit výkonnost na některých plánovacích doménách, především v R2 ∃-Step en- coding.
|
|
|
Vizualizace hmatových a zvukových vjemů
Lukš, Roman ; Zachariáš, Michal (oponent) ; Polok, Lukáš (vedoucí práce)
Cílem této bakalářské práce je návrh a implementace vizualizace hmatových a zvukových vjemů běžících v reálném čase. Vjemy mají sloužit pro orientaci hráče v jednoduché 2D hře místo zraku. Vjemy jsou vizualizovány pomocí shaderů na GPU. Zvukové vjemy jsou implementací simulace vlnění výpočetně nenáročnou explicitní metodou. Hmatový vjem je tvořen pomocí pohyblivých čar. K vykreslování je použita knihovna OpenGL. V práci jsem vytvořil funkční herní prototyp obsahující dvojici vjemů.
|
|
|
Simulace pevných těles
Leitner, Denis ; Milet, Tomáš (oponent) ; Chlubna, Tomáš (vedoucí práce)
Táto práca je zameraná na simuláciu fyziky pevných telies v reálnom čase. Popisuje základné postupy používané pri hernom vývoji zamerané na detekciu kolízie medzi konvexnými mnohostenmi. Ďalej popisuje riešenie zistenej kolízie a spôsob simulácie dynamiky pevných telies. Zaoberá sa takisto aj návrhom a implementáciou simulátoru pevných telies v jazyku C++. Na vykresľovanie scény je použité OpenGL.
|
|
|
Využití SAT solverů v úloze optimalizace kombinačních obvodů
Minařík, Vojtěch ; Mrázek, Vojtěch (oponent) ; Vašíček, Zdeněk (vedoucí práce)
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.
|
|
|
Modelování kooperativního hledání cest
Ježek, Milan ; Surynek, Pavel (vedoucí práce) ; Majerech, Vladan (oponent)
V této práci jsou popsány nové modely pro řešení kooperativního hledání cest (cpf) s požadavkem na minimální makespan a je provedeno jejich experimentální porovnání se stávajícími modely. Nové modely uvedené v práci zkoumají možnosti kódování problému cpf pomocí celočíselného lineárního programování s binárními proměnnými (bip) a jako problém splnitelnosti omezujících podmínek (csp). Při testech se ukázaly hlavně poměrně dobré výsledky nového modelu IP active-edges při vyšším množství agentů, kdy jen mírně zaostával za nejlepším SAT modelem. Nový model pro csp dosáhl nejrychlejších časů v testech s nízkým množstvím překážek a interakcí mezi agenty, zatímco v opačném případě se jeho výkon dramaticky snižoval. Powered by TCPDF (www.tcpdf.org)
|
host ::
RSS.