doc. RNDr. Dušan Knop, Ph.D.

Numerous topics in (computational) social choice are nowadays important parts of various systems in our day to day life. These include, e.g., recommender systems, or distribution of goods stored in food banks. Now, as the use of these crucial tools grows so does the need for efficient computation of solutions to these problems. The main (suggested) toolbox used to pursue this task is the framework of parameterized (or, multivariate) complexity that is becoming more and more popular in the past decades. The practical need for the computation also yields the possibility to a more applied research using, e.g., ILP or SAT solvers. The biggest challenges in the area include problems which are complete for “higher classes” of classical complexity (i.e., possibly above NP); e.g., the Judgement Aggregation problem.

doc. RNDr. Dušan Knop, Ph.D.

RNDr. Radek Hušek, Ph.D.

Department of Theoretical Computer Science

This thesis describes an implementation of the binary minimum heap and formal proofs of the correctness of individual operations. The verified binary heap is then used in Dijkstra's algorithm for finding the shortest path in a graph.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

doc. Ing. Ivan Šimeček, Ph.D.

Department of Computer Systems

This thesis deals with the implementation of the Dinitz algorithm for finding maximum flow in the network and the formal proof of individual functions, that it uses. The theoretical part introduces the reader to the theory of flows in networks and the idea of the Dinitz algorithm. It will also introduce the reader to the Frama-C framework for formal code analysis in the C programming language and the ACSL annotation language, which helps the framework with the verification. The practical part introduces the reader to the methods used to implement the Dinitz algorithm and also clarifies the annotations used for the algorithm verification.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

RNDr. Jiřina Scholtzová, Ph.D.

Department of Theoretical Computer Science

In this work, we study Hedonic games and provide an overview of stability concepts and restrictions of preference profiles. Then, we focus on a version in which the set of agents has been changed by some of the former agents leaving and the same amount of new ones coming, and we are expected to find an updated coalition structure. We restrict the problem to filling the new agents to places that had been emptied by the leaving former agents, and to the subclass of anonymous Hedonic games. We describe a polynomial-time algorithm for finding a strictly core stable coalition structure, and for the case of core stable coalition structure, a slow algorithm for finding it and several methods of transforming the problem to flows in networks.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

Mgr. Michal Opler, Ph.D.

Department of Theoretical Computer Science

This thesis focuses on winner selection in committee election. We provide an overview of voting systems for single-winner and multi-winner election. Winner selection is often computationally hard, therefore we introduce election with structured preferences. In election with structured preferences, the votes are in some way restricted which may help to create more efficient winner selection algorithms. We describe some of the known structured preferences. We provide an overview of the current literature on the topic of structured and nearly structured preferences. We also review current work on committee election with structured preferences and usage of ordered weighted average (OWA) in committee election. We propose polynomial-time algorithms for finding a winning committee for approval election with OWA vector (0, ..., 0, 1) and interval preference restrictions. In such election, a voter approves a committee only if she approves all of its members. We use this property and show two approaches for finding a winning committee.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

Department of Theoretical Computer Science

In the Roommate diversity problem, agents that belong to one of the two types have to be allocated to fixed size rooms based on their preferences, which depend solely on the fraction of agents of their own type among their potential roommates. In this work we study the stability of outcomes with respect to the room size and structured preferences. We provide a new randomized algorithm for finding core stable outcomes and show the results which we have obtained with the algorithm. We have found a small single-peaked instance with empty core and have verified, that every instance of the Roommate diversity problem with room size = 3, all preferences single peaked and number of agents <= 30, room size = 3 and number of agents <= 15, room size = 4, all preferences single peaked and number of agents = 30, admits an outcome that is core stable. We present arguments why we believe that every instance of this problem with room size = 3, room size = 4 and all preferences single peaked, admits an outcome that is core stable.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

Ing. Jiří Smítka

Department of Computer Systems

This thesis explores the possibilities of formal deductive verification of the RSA encryption algorithm. The theoretical part serves as an introduction to the realm of formal deductive verification and its basic concepts, along with a brief survey of current applications of its concepts in industry. Furthermore, the RSA encryption algorithm and the Frama-C verification environment for C-language programs, which uses annotations and automatic systems for formal verification of theorems, are briefly described. The practical part provides a demonstration of application of concepts explored in the theoretical part using an implementation of the RSA algorithm in the C programming language and its partial verification using Frama-C. The final result of this thesis is therefore a partially verified implementation of the RSA algorithm. Some of the possible utility of such an implementation is demonstrated using an example SO/DLL injection attack against one of its components.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

RNDr. Jiřina Scholtzová, Ph.D.

Department of Theoretical Computer Science

The assignment problem is a problem on intersection of mathematical and economical theory. Assignment problem consist of agents and items, the agents express their preferences over items and the goal is to find (in some way) optimal allocation. The assignment problem is very dynamical problem, because lot of others aspects might be taken into consideration. In this example agents have multiple preference lists as presneted in Parameterized Analysis of Assignment Under Multiple Preferences. However we took different approach to the problem than in the article, motivated by the amount of research already done on single preference profile assignment problem, we present synthesising one profile from multiple ones. As well as presenting an algorithm for finding Pareto optimal solution on such profiles. Since the profiles we presented allowed equations between two items, (meaning none of them is preferred over the other) we had to take a slightly different approach. The main focus was to find algorithmic solution with at least polynomial time complexity, which was achieved. We also discuss different aspects of fairness in such assignments. following solutions should be beneficial not only to Assignment Under Multiple Preference as to present a new view on the recently published problem, but also to the Assignment problem with non-strict profiles.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

Ing. Šimon Schierreich

Department of Theoretical Computer Science

Target Set Selection is an NP-hard problem fundamental in the area of viral marketing. Given a social network, the Target Set Selection problem asks for the minimum size set of agents, whose influence ultimately affects everyone in the network. We propose the Fair Target Set Selection problem, whose solution satisfies a fair cost measure rather than a certain solution size. The fair cost enforces a fair distribution of a target set by bounding the maximum number of friends of some agent in a solution. In this work, we study the parameterized complexity of Fair Target Set Selection and show W[1]-hardness with respect to parameters treewidth, feedback vertex set number, and treedepth and W[2]-hardness for its natural parameter fair cost. On the more positive side, we show an FPT algorithm with respect to the combined parameter vertex cover number and fair cost. Our further results arrive when we consider special cases of the threshold functions since we prove NP-hardness when all thresholds are equal to a constant c ≥ 3. Moreover, in the last chapter we give arguments why we believe that might be a polynomial time algorithm for Fair Target Set Selection with majority thresholds on trees.

Thesis on DSpace

RNDr. Dušan Knop, Ph.D.

Ing. Radovan Červený

Department of Theoretical Computer Science

This thesis summarizes known results of the Max Cut problem and introduces a new kernelization algorithm for the Simple Max Cut problem parameterized by vertex cover number of the input graph G bounding the size of the kernel by O(vc(G)^4), where vc(G) denotes vertex cover number of G.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

prof. Ing. Pavel Tvrdík, CSc.

Department of Computer Systems

This thesis deals with introduction into deductive formal verification. The theoretical part introduces the reader to the Frama-C framework for modular analysis of programs written in C, which uses plugins, automatic theorem provers and annotation language ACSL for verification. In the thesis are further explained important parts of the verification environment, it's installation and usage. Methods and strategies that are used are described in more detail and showed on examples. The result of thesis is a fully verified algorithm for finding a minimum spanning tree of a graph.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

Ing. Daniel Vašata, Ph.D.

Department of Applied Mathematics

The maps of elections framework is a methodology for visualizing and analyzing election datasets. So far, this framework was restricted to collections of election datasets that have equal numbers of candidates. In this thesis, we extend this framework to be able to deal with datasets containing different numbers of candidates. We do this in two ways: we extend an already existing positionwise distance, and we also develop the idea and implementation of a feature distance. We test the new distances on synthetic data generated using the Mapel package.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

doc. RNDr. Ing. Petr Zemánek, CSc.

Department of Computer Systems

Union-Find is a data structure that can be used for tasks that require set union and checking to which set an element belongs. Software developers do not implement those data structures on their own. They prefer to look for them online. The problem is, that it is difficult to verify the correctness of the implementation. This thesis focuses on analyzing the Union-Find data structure, ways of optimized implementation, verification, and performance comparison of selected implementations.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

RNDr. Jiřina Scholtzová, Ph.D.

Department of Theoretical Computer Science

In this bachelor thesis, we introduce and examine the Multi-Graph Multi-Constrained Optimal Path (MGMCOP) problem. This problem is related to the Traveling Salesman Problem (TSP), which is known to be an NP-complete problem. The MGMCOP problem has wide-ranging applications in diverse real-life scenarios, particularly in sparse networks where computational efficiency is very important. We present a dynamic programming algorithm that yields pseudo-polynomial time complexity for solving this problem. However, the main part of our work is about imposing specific constraints on the input data. These constraints, carefully designed and implemented, reduce the time complexity of our algorithm to be polynomial. This complexity reduction is achieved without sacrificing solutions accuracy and practical utility in sparse networks.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

Mgr. Michal Opler, Ph.D.

Department of Theoretical Computer Science

We study the following model of opinion spread in a social network. In the beginning, some individuals in the network adopt a concrete opinion (for example, they are bribed to adopt it). Next, in discrete rounds, the opinion spreads throughout the network in the following way. An individual that has not yet adopted the opinion, adopts it if a~sufficient number of its direct neighbors possess the opinion. The task is to initially influence a~small number of individuals such that the opinion floods the entire network. This model corresponds to a~notorious hard problem called Target Set Selection. In this work, we address geometric graphs, in particular, unit disk graphs. We show that even in this class Target Set Selection remains NP-hard, even if maximum degree of the underlying graph is 4 and thresholds are at most 2. We also show NP-hardness of Target Set Selection in the majority and unanimous threshold settings. En route, we show similar hardness results for related classes of graphs such as disk contact or grid graphs.

Thesis on DSpace

RNDr. Dušan Knop, Ph.D.

doc. Ing. Štěpán Starosta, Ph.D.

Department of Theoretical Computer Science

A simple undirected graph G=(V,E) is said to be a sum graph if there is an injective function s: V - N such that for every u,v [?] V there is an edge {u,v} in E if and only if there exists a vertex w [?] V such that s(w) = s(u) + s(v). It is easy to see that none connected graph is a sum graph since the vertex v with the largest label is not adjacent to any other vertex. Therefore, we investigate the sum number of a graph G, which is the minimum number of isolated vertices we must add to G to obtain a sum graph. We study this problem in its entirety. We provide complete definitions of sum graphs and their properties. For some graph families, we investigate their sum numbers and provide exact labeling algorithms to find an optimal labeling. In the last part of this thesis, we present exact exponential algorithms that find a sum number for an arbitrary graph.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

RNDr. Ondřej Suchý, Ph.D.

Department of Theoretical Computer Science

Microaggregation is a classical statistical disclosure control technique that requires the input data to be partitioned into clusters while adhering to specified size and distance constraints. We explore the problem when the data points are embedded into a network that specifies the distances. Additionally, we consider the case when the clusters are connected. We use a combination of input parameters (maximum cluster size, maximum distance) and structural parameters (vertex cover, treewidth, treedepth) to achieve or rule out tractability in various settings. Namely, we propose a dynamic programming algorithm for the connected version. Further, we show FPT algorithms parameterized by vertex cover and maximum distance based on integer linear programming for both versions of the problem. On the other hand, we show that the connected version is W[1]-hard with respect to treewidth and maximum distance. For disconnected clusters, the problem is also W[1]-hard when parameterized by the vertex cover number. Lastly, we establish W[1]-hardness of the problem Equitable Connected Partition when parameterized by treedepth.

Thesis on DSpace

doc. RNDr. Dušan Knop, Ph.D.

RNDr. Petr Olšák

Department of Applied Mathematics

In dynamically changing world, we cannot expect our preferences to be constantly unchanged under outside factors. Hence, we need solutions of our problems to adapt well to changes. In \textsc{Stable Marriage} problem, sets of men and women are being matched according to their \textit{preferences}. The goal is to find a matching, where no man and woman both prefer each other over their current partners. We study the effect of dynamicaly changing preferences of these men and women and define \textsc{Temporal Stable Marriage} problem that adresses these changes. This problem tries to find a matching, where at most \textit{k} pairs prefer each other over their current partners under multiple preference profiles. We prove that this problem is \textit{NP-complete}, even with constant value of \textit{k}, and propose algorithms that might be a few observations away from being able to find a valid solution in time better than naive brute force method.

Thesis on DSpace