|
|
Řazení manipulací pro mořící linky
Plšek, Michal ; Tinka, Jan (oponent) ; Kanich, Ondřej (vedoucí práce)
Tato práce řeší problém plánování pohybů jednoho nebo více jeřábů při přesunu produktů mezi vanami mořicí linky. Harmonogramy zpracování jednotlivých produktů ve vanách jsou vytvořeny pomocí modifikované Shifting bottleneck heuristiky, zabraňující střetu produktů ve vanách. Pro prohledávání celého prostoru řešení je použit genetický algoritmus NSGA-II. Nad optimalizační procesem je postavena webová aplikace, která umožňuje správu a prohlížení produktů, částí mořicí linky, historie úloh a konfiguračních parametrů úlohy. Aplikace u úloh menšího rozsahu dosahuje zefektivnění až 30-45 % ve srovnání s naivními harmonogramy operací namáčení. Výsledkem této práce je funkční aplikace, na jejímž základě je možné postavit optimalizační aplikaci v jazyce C++ použitelnou k řešení obdobného problému o větším rozsahu.
|
|
|
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.
|
|
|
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.
|
|
|
Řazení manipulací pro mořící linky
Plšek, Michal ; Tinka, Jan (oponent) ; Kanich, Ondřej (vedoucí práce)
Tato práce řeší problém plánování pohybů jednoho nebo více jeřábů při přesunu produktů mezi vanami mořicí linky. Harmonogramy zpracování jednotlivých produktů ve vanách jsou vytvořeny pomocí modifikované Shifting bottleneck heuristiky, zabraňující střetu produktů ve vanách. Pro prohledávání celého prostoru řešení je použit genetický algoritmus NSGA-II. Nad optimalizační procesem je postavena webová aplikace, která umožňuje správu a prohlížení produktů, částí mořicí linky, historie úloh a konfiguračních parametrů úlohy. Aplikace u úloh menšího rozsahu dosahuje zefektivnění až 30-45 % ve srovnání s naivními harmonogramy operací namáčení. Výsledkem této práce je funkční aplikace, na jejímž základě je možné postavit optimalizační aplikaci v jazyce C++ použitelnou k řešení obdobného problému o větším rozsahu.
|
|
|
Application of Branch and Bound Approach to Parametric Interval Linear Systems
Szabó, Adam ; Horáček, Jaroslav (vedoucí práce) ; Rada, Miroslav (oponent)
Tato práce se zaobírá parametrickými intervalovými lineárními soustavami. Branch and bound metodou a různými námi implementovanými prořezávacími podmínkami jsme dostali jejich množinu řešení. Přesněji jsme ji popsali po- mocí n-rozměrných boxů, které jsme získali díky využitým metodám. Seznámili jsme se se základními pojmy ohledně intervalů a lineárních soustav. Následně jsme zpracovávali získané boxy řešení vícerými metodami s cílem optimali- zovat jejich počet. Součástí práce je i porovnání jednotlivých prořezávacích podmínek na parametrických soustavách s různým počtem parametrů. Uve- dené algoritmy byly implementované do intervalového balíku Lime s možností jednoduché vizualizace získaných řešení. 1
|
|
|
Využití grafických procesorů v úlohách celočíselného programování
Hájek, Jan ; Fábry, Jan (vedoucí práce) ; Černý, Michal (oponent)
Široká podskupina okružních úloh z teorie grafů je častým problémem, který řeší přepravní firmy, letecké společnosti, hi-tech firmy pro plánování výroby plošných spojů nebo společnosti z úplně jiného hospodářského odvětví. Během dřívějších nejrůznějších výzkumů těchto úloh bylo provedeno mnoho analýz a představeno mnoho způsobů řešení, jejichž nástin je uveden v této práci. Některé z nich podávají lepší či horší výsledky v delším či kratším výpočetním čase. Přestože se výkon procesorů a současných technologií nadále zvyšuje, je s některými algoritmy obtížné se dopočítat výsledku v rozumném čase. Proto se práce zabývá otázkou, zda je možné nalézt vhodný algoritmus, který by bylo možné aplikovat na jiné a rychlejší struktury výpočetních jednotek tak, aby se zajistilo mnohonásobné zvýšení výpočetní rychlosti než doposud. Pro tento výzkum byl vytvořen a implementován testovací algoritmus metody větvení a mezí s maticovou redukcí sazeb, který byl podroben počítačovým experimentálním testům, jejichž důsledky jsou zde uvedeny.
|
host ::
RSS.