|
|
Solving Boolean satisfiability problems
Balyo, Tomáš ; Surynek, Pavel (advisor) ; Barták, Roman (referee)
In this thesis we study the possibilities of decomposing Boolean formulae into connected components. For this reason, we introduce a new concept - component trees. We describe some of their properties and suggest some applications. We designed a class of decision heuristics for SAT solvers based on component trees and experimentally examined their performance on benchmark problems. For this purpose we implemented our own solver, which uses the state-of-theart SAT solving algorithms and techniques.
|
|
|
Grid-Based Path Planning
Novella, Tomáš ; Balyo, Tomáš (advisor) ; Martínek, Vladislav (referee)
This thesis deals with effective ways of pathfinding in grid-based graphs. In the first part we pointed out the most important approaches to finding the shortest path. In the second part we proposed an algorithm that improves the speed of pathfinding in some special cases of grid-based graph. In the end we proved it by providing a series of experiments. Powered by TCPDF (www.tcpdf.org)
|
|
|
Unified Editor for CEGUI
Preisler, Martin ; Babka, Martin (advisor) ; Balyo, Tomáš (referee)
This thesis presents a free software GUI application called the CEGUI Unified Editor. The application is mainly written in Python and is licensed under GPLv3. Its purpose is to create and modify assets of graphical interfaces made with the CEGUI library. Features include project management, imageset editing and layout editing. Data for older versions of CEGUI are transparently converted using compatibility layers. Big emphasis is put on ease of use, collaboration between multiple content authors and portability.
|
|
|
Real-time strategy game with artificial intelligence
Fanta, Petr ; Balyo, Tomáš (advisor) ; Dvořák, Filip (referee)
The aim of this thesis is to create a real-time strategy game with artificial intelligence in 3D environment. The thesis includes theoretical analysis of combat real-time strategy games, methods for implementing artificial intelligence in this kind of games, and the basic knowledge of 3D environment implementation. A simple 3D real-time strategy game with artificial intelligence has been implemented as a part of this this thesis.
|
|
|
Alignment of photographies for HDR using key points.
Viktorín, Daniel ; Bardiovský, Vojtěch (advisor) ; Balyo, Tomáš (referee)
The thesis deals with the alignment of manually captured photographs which are to be used for HDR merging. It focuses on available methods, describes their drawbacks and presents an algorithm capable of detection of global translation, rotation and scaling within pairs of input photographs. This algorithm is based on searching for suitable key points among single photographs, their weighted pairing and final calculation of the transformation. The enclosed application can perform direct HDR merging of the aligned photographs which is used to compare the results of registration with other methods and available applications. Powered by TCPDF (www.tcpdf.org)
|
|
|
Efficient SAT Solver
Balyo, Tomáš ; Surynek, Pavel (advisor) ; Mareš, Martin (referee)
The boolean satisfaction problem (SAT) is one of the most important and most studied problems of artificial intelligence. Many theoretical and real life problems are transformed to SAT and solved using a SAT solver. During the research for this thesis two SAT solvers were developed. They are described and compared with several of today's state-of-art SAT solvers. The presented solvers in many cases outperform the 2007's SAT competition winner R-sat and other famous SAT solvers. These two new solvers thank their speed to the implementation techniques used and to their decision heuristic, which is very efficient while absolutely costless.
|
|
|
Graph labeling
Böhm, Martin ; Mareš, Martin (advisor) ; Balyo, Tomáš (referee)
We introduce the concept of adjacency labeling schemes and recent results in the area. These schemes have practical application in parallel algorithm design and they relate to the theory of universal graphs. We concentrate on the modern technique of "Traversal and Jumping". We present a less technical proof of its correctness as well as correcting some errors in the original proof. We also apply brute-force algorithms to find small induced-universal graphs. 1
|
|
|
Third-person flight action game with map generator
Nevolová, Kateřina ; Balyo, Tomáš (advisor) ; Krajíček, Václav (referee)
The goal of this thesis was to design and create a third-person flight action game in 3D. The theoretical part of this work includes analysis of the action game environment, the concept of the physical model for the use in movement and orientation in 3D, discussion about artificial intelligence used in this genre and specification of own map format. This work also includes the implementation of such game with a compatible map generator.
|
|
|
Finding Minimum Satisfying Assignments of Boolean Formulas
Švancara, Jiří ; Balyo, Tomáš (advisor) ; Trunda, Otakar (referee)
In this thesis we examine algorithms and techniques used for solving Boolean satisfiability (SAT). Then we inspect the possibility to use them in solving the weighted short SAT problem, which is a generalization of the satisfiability problem. Given that each variable has a weight, this generalization is the problem of finding a satisfying truth assignment while using the smallest sum of weights. To solve this problem, we introduce three truth assignments of variables - True, False and Unassign. We show that not all algorithms and techniques used in modern SAT solvers can be used in our program. Those that can be converted, will be implemented using our three truth assignments. This will yield several versions of our new solver, which will be compared. Powered by TCPDF (www.tcpdf.org)
|
|
|
Coordinated pathfinding with formations
Obrázek, Václav ; Surynek, Pavel (advisor) ; Balyo, Tomáš (referee)
The topic of cooperative pathfinding with the extension of formations is addressed in this thesis. The problem of cooperative pathfinding with formations was formally defined and a new scalable hierarchical modular solving algorithm named APriCA was introduced and implemented. For testing and benchmarking purposes an environment called ChessWars was developed. In order to measure the quality of maintaining formations we introduced a new quantity named "fragmentation". The APriCA algorithm performed better than external domain independent planners such as LPG, Blackbox and SASE in all aspects. In comparison with the LRA* algorithm the solutions found by APriCA were of better quality and with certain parameters settings were found faster.
|
guest ::
