|
|
Modern ways to design fully distributed, decentralized and stealthy worms
Szetei, Norbert ; Krištofič, Milutín (advisor) ; Balyo, Tomáš (referee)
The thesis deals with the study of the computer worm meeting several criteria (it should be fully distributed, decentralized and stealthy). These conditions lead to anonymity, longevity and better security of our worm. After presenting the recently used architectures and new technologies we analyse the known implementations. We propose the solutions with the new design together with the possible ways of improvements. In the next chapter we study biological concepts suitable for the new replication mode, where we implement the key concepts of functionality in a higher programming language. At design we have considered as important to be platform independent, so it is possible for the worm to spread in almost every computer environment, in dependence of implementation of the required modules. Powered by TCPDF (www.tcpdf.org)
|
|
|
Comparing reactive techniques to classical planning for intelligent virtual agents
Černý, Martin ; Gemrot, Jakub (advisor) ; Balyo, Tomáš (referee)
Many contemporary computer games can be described as dynamic real-time simulations inhabited by autonomous intelligent virtual agents (IVAs) where most of the environment structure is immutable and navigating through the environment is one of the most common activities. Though controlling the behaviour of such agents seems perfectly suited for action planning techniques, planning is not widely adopted in existing games. This paper attempts to answer the question whether the current academic planning technology is ready for integration to existing games and under which conditions. The paper compares reactive techniques to classical planning in handling the action selection problem for IVAs in game-like environments. Several existing classical planners that occupied top positions in the International Planning Competition were connected to the virtual environment of Unreal Development Kit via the Pogamut platform. Performance of IVAs employing those planners and IVAs with reactive architecture was measured on a class of game like test environments under different levels of external interference. It was shown that agents employing classical planning outperform reactive agents only if the size of the planning problem is small or if the environment changes are either hostile to the agent or not very frequent.
|
|
|
Experiment management system
Faryad, Jakub ; Balyo, Tomáš (advisor) ; Podzimek, Andrej (referee)
The aim of the thesis is to design and implement a system for managing and running and comparing the results of programs for solving computational problems. The application distributes the experiments on predefined computer pools through the ssh and scp protocols. The system allows multiple user groups to share input date, upload new versions of programs and schedule their execution. The results are stored in a database, they can be downloaded at any time in various formats and graphically compared. The result is a multi-layer web application based on the J2EE platform.
|
|
|
Modelling and Solving Problems Using SAT Techniques
Balyo, Tomáš ; Barták, Roman (advisor) ; Železný, Filip (referee) ; Biere, Armin (referee)
Solving planning problems via translation to satisfiability (SAT) is one of the most successful approaches to automated planning. In this thesis we describe several ways of encoding a planning problem represented in the SAS+ formalism into SAT. We review and adapt existing encoding schemes as well as introduce new original encodings. We compare the encodings by calculating upper bounds on the size of the formulas they produce as well as by running extensive experiments on benchmark problems from the 2011 International Planning Competition (IPC). In the experimental section we also compare our encodings with the state-of-the-art encodings of the planner Madagascar. The experiments show, that our techniques can outperform these state-of-the-art encodings. In the presented thesis we also deal with a special case of post-planning optimization -- elimination of redundant actions. The elimination of all redundant actions is NP-complete. We review the existing polynomial heuristic approaches and propose our own heuristic approach which can eliminate a higher number and more costly redundant actions than the existing techniques. We also propose a SAT encoding for the problem of plan redundancy which together with MaxSAT solvers allows us to solve the problem of action elimination optimally. Experiments done with...
|
|
|
Solving Boolean satisfiability problems
Balyo, Tomáš
In this thesis we study the possibilities of decomposing Boolean formulae into connected components. or 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-the-art SAT solving algorithms and techniques.
|
|
|
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)
|
|
|
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)
|
|
|
Effective encoding of the Hidato and Numbrix puzzles to their CNF representation
Bartoš, Samuel ; Balyo, Tomáš (advisor) ; Vodrážka, Jindřich (referee)
Although Boolean satisfiability problem (SAT) is NP-complete, thanks to the progress in the performance of SAT solvers many other problems can be solved efficiently by encoding them into Boolean formulas. In this thesis this method is applied to find the solution to Hidato and Numbrix puzzles. We present various encoding techniques and describe an implementation of an application designed to construct them. The efficiency of individual encodings together with their effect on the performance of several SAT solvers is examined. The results of conducted experiments indicate that the efficiency of encoding can change from solver to solver and that the best choice of encoding-solver combination depends heavily on the size and type of puzzle. Powered by TCPDF (www.tcpdf.org)
|
|
|
Modelling and Solving Problems Using SAT Techniques
Balyo, Tomáš ; Barták, Roman (advisor) ; Železný, Filip (referee) ; Biere, Armin (referee)
Solving planning problems via translation to satisfiability (SAT) is one of the most successful approaches to automated planning. In this thesis we describe several ways of encoding a planning problem represented in the SAS+ formalism into SAT. We review and adapt existing encoding schemes as well as introduce new original encodings. We compare the encodings by calculating upper bounds on the size of the formulas they produce as well as by running extensive experiments on benchmark problems from the 2011 International Planning Competition (IPC). In the experimental section we also compare our encodings with the state-of-the-art encodings of the planner Madagascar. The experiments show, that our techniques can outperform these state-of-the-art encodings. In the presented thesis we also deal with a special case of post-planning optimization -- elimination of redundant actions. The elimination of all redundant actions is NP-complete. We review the existing polynomial heuristic approaches and propose our own heuristic approach which can eliminate a higher number and more costly redundant actions than the existing techniques. We also propose a SAT encoding for the problem of plan redundancy which together with MaxSAT solvers allows us to solve the problem of action elimination optimally. Experiments done with...
|
|
|
Solving Boolean satisfiability problems
Balyo, Tomáš
In this thesis we study the possibilities of decomposing Boolean formulae into connected components. or 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-the-art SAT solving algorithms and techniques.
|
guest ::
