|
|
Mobilní aplikace pro rozvrhovaní disciplín na dětském táboře
Holub, Ondřej ; Martiček, Štefan (oponent) ; Češka, Milan (vedoucí práce)
Práce se zabývá návrhem a tvorbou mobilní aplikace usnadňující plánování aktivit na dětském táboře na základě preferencí účastníků. Aplikace je implementována způsobem, který zajišťuje minimalizaci konfliktů preferencí s ohledem na dodatečná, uživatelem definovaná omezení. Pro efektivní zadávání vstupních dat je využito skenování karet účastníků, které obsahují QR kódy. Samotný proces hledání optimálního rozdělení je formalizován jako problém barvení grafu a je implementován s využitím metody větví a mezí. Vytvořený systém nevyžaduje pro své fungování žádné další zařízení, veškerý výpočet běží přímo na mobilním telefonu uživatele. Díky systému byl významně urychlen a zjednodušen proces plánování rozvrhů na dětských táborech.
|
|
|
Formal Analysis of Neural Networks
Hudák, David ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Today, the area where we can use deep learning is becoming broader. It includes safety-critical domains such as traffic or healthcare, and the need for its verification grows. However, sufficient verification toolkits for neural networks, the leading deep learning approach, are still in development. State-of-the-art algorithms now can not verify commonly used deep networks. In this paper, we focus on one of the state-of-the-art solutions, VeriNet. More generally, we focused on the symbolic approach of local robustness analysis. This approach usually relies on creating, processing, and refining the neural network representation, and we focused on the refinement phase. We primarily dealt with the branch and bound algorithm, which in this toolkit splits node inputs in a network to create smaller sub-problems. For this algorithm, we proposed and implemented new split node selection strategies. Specifically, we designed memory-based, alternating, and semi-hierarchical strategies. We achieved significant improvements in the scalability of the VeriNet toolkit. One of our approaches can solve more complex cases and significantly improve already solved cases' performance. Moreover, we discovered an anomaly in the behavior of the verification algorithm we named branch implosions, which led to extreme speed up for some cases. In addition, we extended the set of performed network benchmarks with models from the Marabou package.
|
|
|
Optimalizace plánování výroby
Kovářová, Karolína ; Šeda, Miloš (oponent) ; Kůdela, Jakub (vedoucí práce)
Tato diplomová práce pojednává o plánování výroby a její optimalizaci. Plánování hraje důležitou roli v širokém spektru oblastí – např. ve výrobním průmyslu, službách, dopravě a distribuci. Rešeršní část je věnována stručné historii a vývoji plánovacích úloh, dále pak klasifikaci plánovacích úloh a základům optimalizace. Je vybrána úloha pro praktickou část a popsány metody použitelné pro její optimalizaci. Vybrané algoritmy jsou implementovány, aplikovány na pět testovacích instancí a vzájemně porovnány.
|
|
|
Formal Analysis of Neural Networks
Hudák, David ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Today, the area where we can use deep learning is becoming broader. It includes safety-critical domains such as traffic or healthcare, and the need for its verification grows. However, sufficient verification toolkits for neural networks, the leading deep learning approach, are still in development. State-of-the-art algorithms now can not verify commonly used deep networks. In this paper, we focus on one of the state-of-the-art solutions, VeriNet. More generally, we focused on the symbolic approach of local robustness analysis. This approach usually relies on creating, processing, and refining the neural network representation, and we focused on the refinement phase. We primarily dealt with the branch and bound algorithm, which in this toolkit splits node inputs in a network to create smaller sub-problems. For this algorithm, we proposed and implemented new split node selection strategies. Specifically, we designed memory-based, alternating, and semi-hierarchical strategies. We achieved significant improvements in the scalability of the VeriNet toolkit. One of our approaches can solve more complex cases and significantly improve already solved cases' performance. Moreover, we discovered an anomaly in the behavior of the verification algorithm we named branch implosions, which led to extreme speed up for some cases. In addition, we extended the set of performed network benchmarks with models from the Marabou package.
|
|
|
Řešení lineárních úloh s celočíselnými omezeními v GAMSu
Škoda, Štěpán ; Branda, Martin (vedoucí práce) ; Kopa, Miloš (oponent)
V předložené práci studujeme problémy celočíselné lineární opti- malizace a to nejprve z hlediska teoretického (část I) a následně na základě empirických údajů (část II). První sekce vysvětluje, čím se tento obor zabývá a kde se aplikuje. Druhá a třetí obsahují okomentované matematické formu- lace úloh, definice a věty potřebné k pochopení metod pro řešení obecných lineárních optimalizačních úloh. V poslední sekci první části se seznámíme s dvěma nejznámějšími skupinami algoritmů, které používá komerční software. Druhá část podává bližší informace o jedné internetové knihovně obsahující některé praktické problémy, které bylo v minulosti potřeba řešit. Dále se zde vyskytují sekce pojednávající o solverech a pokročilých volbách systému GAMS. V poslední sekci jsou uvedena data získaná při řešení úloh pomocí různých kódů (solverů) softwaru. 1
|
|
|
Mobilní aplikace pro rozvrhovaní disciplín na dětském táboře
Holub, Ondřej ; Martiček, Štefan (oponent) ; Češka, Milan (vedoucí práce)
Práce se zabývá návrhem a tvorbou mobilní aplikace usnadňující plánování aktivit na dětském táboře na základě preferencí účastníků. Aplikace je implementována způsobem, který zajišťuje minimalizaci konfliktů preferencí s ohledem na dodatečná, uživatelem definovaná omezení. Pro efektivní zadávání vstupních dat je využito skenování karet účastníků, které obsahují QR kódy. Samotný proces hledání optimálního rozdělení je formalizován jako problém barvení grafu a je implementován s využitím metody větví a mezí. Vytvořený systém nevyžaduje pro své fungování žádné další zařízení, veškerý výpočet běží přímo na mobilním telefonu uživatele. Díky systému byl významně urychlen a zjednodušen proces plánování rozvrhů na dětských táborech.
|
|
|
Řešení lineárních úloh s celočíselnými omezeními v GAMSu
Škoda, Štěpán ; Branda, Martin (vedoucí práce) ; Kopa, Miloš (oponent)
V předložené práci studujeme problémy celočíselné lineární opti- malizace a to nejprve z hlediska teoretického (část I) a následně na základě empirických údajů (část II). První sekce vysvětluje, čím se tento obor zabývá a kde se aplikuje. Druhá a třetí obsahují okomentované matematické formu- lace úloh, definice a věty potřebné k pochopení metod pro řešení obecných lineárních optimalizačních úloh. V poslední sekci první části se seznámíme s dvěma nejznámějšími skupinami algoritmů, které používá komerční software. Druhá část podává bližší informace o jedné internetové knihovně obsahující některé praktické problémy, které bylo v minulosti potřeba řešit. Dále se zde vyskytují sekce pojednávající o solverech a pokročilých volbách systému GAMS. V poslední sekci jsou uvedena data získaná při řešení úloh pomocí různých kódů (solverů) softwaru. 1
|
|
|
Kavdratický přiřazovací problém a jeho řešení
Nováčková, Monika ; Jablonský, Josef (vedoucí práce) ; Fábry, Jan (oponent)
Kvadratický přiřazovací problém je jednou z nejsložitějších úloh kombinatorické optimalizace. Jedná se o velmi rozsáhlou rozhodovací úlohu třídy NP-complete. Poprvé tento problém představili v roce 1957 Koopmans a Beckman. Od té doby byly zkoumány různé metody řešení tohoto problému. Jedná se o nejrůznější exaktní ale i heuristické algoritmy. V této práci je podrobněji popsán jeden z exaktních algoritmů tzv. metoda větví a mezí (branch and bound algorithm) založená na Gilmore Lawlerově způsobu výpočtu dolních mezí. Dále jsou zde popsány některé aplikační oblasti kvadratického přiřazovacího problému. Jedná se například o úlohu, jak nejlépe rozmístit jednotlivé kliniky a zařízení v areálu nemocnice tak, aby pacienti celkově během svého pobytu v nemocnici museli překonat, co nejmenší vzdálenost mezi jednotlivými klinikami, nebo jak uspořádat jednotlivé komponenty v počítači na desce motherboard tak, aby celkový součin množství signálů a vzdálenosti, kterou musí data překonat, byl co nejmenší.
|
host ::
RSS.