|
|
Mobile Application for Scheduling Activities at Summer Camps
Holub, Ondřej ; Martiček, Štefan (referee) ; Češka, Milan (advisor)
The main goal of this thesis is to design and implement a mobile application assisting in scheduling activities at summer camps taking into account the preferences of camp participants. This is done in a way that ensures the minimization of conflicts with respect to user-defined constraints. QR code scanning is used as an effective method of data input. The main process of finding an optimal solution is formalized as a graph colouring problem and is implemented using the branch and bound method. The created system does not require any other device for its functioning, all the necessary calculations are being executed on a mobile phone of the user. This system has significantly accelerated and simplified the process of scheduling activities at summer camps.
|
|
|
Formal Analysis of Neural Networks
Hudák, David ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
Škála oblastí, ve kterých se dnes můžeme setkat s hlubokým učením, se velmi rychle rozrůstá. Zasahuje už dokonce i mezi bezpečnostně kritické oblasti jako doprava či lékařství, a tak narůstá nutnost takové systémy verifikovat. Nicméně, dostatečně škálovatelné nástroje pro verifikaci neuronových sítí, které tvoří hlavní přístup k hlubokému učení, jsou stále ve vývoji. Dnešní řešení tak nejsou schopny verifikovat dostatečně hluboké sítě. Z toho důvodu jsme se zaměřili na jeden ze současných nástrojů, VeriNet, a pokusili jsme jej vylepšit. Obecněji jsme se zaměřili na symbolický přístup k analýze lokální robustnosti. Tento přístup běžně spočívá na vytvoření, zpracování a přepracování reprezentace neuronové sítě, přičemž my jsme se zaměřili na fázi přepracování. Primárně jsme se zabývali algoritmem větví a mezí, který spočívá v rozdělování vstupů dílčích síťových uzlů k vytváření menších podproblémů. Specificky jsme navrhli nové paměťové, alternující a semi-hierarchické strategie. Při experimentování jsme dosáhli výrazných vylepšení nástroje VeriNet. Jeden z našich přístupů je tak schopen řešit více komplexních případů a také vylepšuje zpracování již řešitelných případů. K tomu jsme navíc narazili na anomálie pracovně nazvané jako imploze větví, které vedou k extrémnímu urychlení některých případů. V rámci této práce jsme také rozšířili set síťových benchmarků s modely z balíku nástroje Marabou.
|
|
|
Production scheduling optimization
Kovářová, Karolína ; Šeda, Miloš (referee) ; Kůdela, Jakub (advisor)
This master’s thesis deals with production scheduling and its optimization. Scheduling plays an important role in a wide variety of areas – e.g., manufacturing, services, transport, and distribution. The theoretical part is dedicated to a brief historical overview and development of scheduling problems, then the classification of these problems and the basics of optimization. A scheduling task for the practical part is selected and methods applicable for its optimization are described. Selected algorithms are implemented, applied to five test instances, and then compared.
|
|
|
Formal Analysis of Neural Networks
Hudák, David ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
Škála oblastí, ve kterých se dnes můžeme setkat s hlubokým učením, se velmi rychle rozrůstá. Zasahuje už dokonce i mezi bezpečnostně kritické oblasti jako doprava či lékařství, a tak narůstá nutnost takové systémy verifikovat. Nicméně, dostatečně škálovatelné nástroje pro verifikaci neuronových sítí, které tvoří hlavní přístup k hlubokému učení, jsou stále ve vývoji. Dnešní řešení tak nejsou schopny verifikovat dostatečně hluboké sítě. Z toho důvodu jsme se zaměřili na jeden ze současných nástrojů, VeriNet, a pokusili jsme jej vylepšit. Obecněji jsme se zaměřili na symbolický přístup k analýze lokální robustnosti. Tento přístup běžně spočívá na vytvoření, zpracování a přepracování reprezentace neuronové sítě, přičemž my jsme se zaměřili na fázi přepracování. Primárně jsme se zabývali algoritmem větví a mezí, který spočívá v rozdělování vstupů dílčích síťových uzlů k vytváření menších podproblémů. Specificky jsme navrhli nové paměťové, alternující a semi-hierarchické strategie. Při experimentování jsme dosáhli výrazných vylepšení nástroje VeriNet. Jeden z našich přístupů je tak schopen řešit více komplexních případů a také vylepšuje zpracování již řešitelných případů. K tomu jsme navíc narazili na anomálie pracovně nazvané jako imploze větví, které vedou k extrémnímu urychlení některých případů. V rámci této práce jsme také rozšířili set síťových benchmarků s modely z balíku nástroje Marabou.
|
|
|
Solving mixed-integer linear programming problems in GAMS
Škoda, Štěpán ; Branda, Martin (advisor) ; Kopa, Miloš (referee)
In the present work we study the problems of integer linear optimi- zation, at first from the theoretical point of view (Part I) and subsequently on the basis of empirical data (Part II). First section explains with what this field deals with and where is applied. Other sections contain annotated mathematical formulation of problems, definitions and theorems needed to understand the general methods for solving integer linear programs. In the last section of Part I, we introduce the two best known groups of algorithms that are used by commercial software. The second part provides more details on an Internet library that contains some practical problems, that has been needed to be solved in the past. Furthermore, there are sections dealing with solvers and the advanced options of GAMS. The last section presents data obtained in the course of solving problems using several codes (solvers) of software. 1
|
|
|
Mobile Application for Scheduling Activities at Summer Camps
Holub, Ondřej ; Martiček, Štefan (referee) ; Češka, Milan (advisor)
The main goal of this thesis is to design and implement a mobile application assisting in scheduling activities at summer camps taking into account the preferences of camp participants. This is done in a way that ensures the minimization of conflicts with respect to user-defined constraints. QR code scanning is used as an effective method of data input. The main process of finding an optimal solution is formalized as a graph colouring problem and is implemented using the branch and bound method. The created system does not require any other device for its functioning, all the necessary calculations are being executed on a mobile phone of the user. This system has significantly accelerated and simplified the process of scheduling activities at summer camps.
|
|
|
Solving mixed-integer linear programming problems in GAMS
Škoda, Štěpán ; Branda, Martin (advisor) ; Kopa, Miloš (referee)
In the present work we study the problems of integer linear optimi- zation, at first from the theoretical point of view (Part I) and subsequently on the basis of empirical data (Part II). First section explains with what this field deals with and where is applied. Other sections contain annotated mathematical formulation of problems, definitions and theorems needed to understand the general methods for solving integer linear programs. In the last section of Part I, we introduce the two best known groups of algorithms that are used by commercial software. The second part provides more details on an Internet library that contains some practical problems, that has been needed to be solved in the past. Furthermore, there are sections dealing with solvers and the advanced options of GAMS. The last section presents data obtained in the course of solving problems using several codes (solvers) of software. 1
|
|
|
The quadratic assignment problem and its solution
Nováčková, Monika ; Jablonský, Josef (advisor) ; Fábry, Jan (referee)
The QAP (quadratic assignment problem) is one of the most involved combinatorial optimization problems. This formidable decision problem is included in the complexity class called NP-complete. The QAP has been first time introduced by Koopmans and Beckman in year 1957. Since then the various methods for solving this problem have been investigated. The studied methods include both: exact algorithms and heuristic methods. Some of them will be shortly described in this paper. One of them, the branch and bound algorithm based on Gilmore Lawler bounds will be analyzed in detail. View applications of this problem will be also discussed. Described applications include the problem of localization of the departments or clinics in a hospital in order to minimize the total traveling distance among clinics by patients. Another described example of application of this problem is the task how to place the components on a computer motherboard optimally.
|
guest ::
