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

Mnoho témat studovaných v rámci výpočetní sociální volby nalezlo v současné době již nespočet aplikací. Abychom vyjmenovali jen několik z nich: doporučovací systémy nebo rozdělování prostředků z potravinových bank. S tím, jak rostou nároky na používané systémy, zároveň roste potřeba efektivních algoritmů pro tyto a příbuzné problémy; speciálně pak podrobné studium jejich vlastností a výpočetní složitosti. Hlavním paradigmatem pro toto studium bude tzv. parametrizovaná složitost (též známá jako multivarietní analýza složitosti algoritmů), která se již řadu let úspěšně používá nejen v tomto oboru. Zároveň je třeba se zaměřit na praktická řešení na reálných datech, na které zle očekávat úspěšné nasazení dlouhodobě vyvíjených nástrojů jakými bezpochyby jsou ILP či SAT řešiče. Zároveň je dobré podotknout, že toto odvětví skrývá i velké výzvy v podobě problémů, které jsou úplné pro “vyšší třídy” polynomiální hierarchie. Takovým problémem je například tzv. Judgement Aggregation.

RNDr. Dušan Knop, Ph.D.

Ing. Radovan Červený

Katedra teoretické informatiky

Tato práce shrnuje dosavadní výzkum problému Max Cut a představuje nový kernelizační algoritmus pro Simple Max Cut problém parametrizovaný velikostí minimálního vrcholového pokrytí vstupního grafu G omezující velikost jádra funkcí O(vc(G)^4), kde vc(G) označuje velikost minimálního vrcholového pokrytí grafu G.

Práce na DSpace

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

Ing. Václav Blažej, Ph.D.

Katedra teoretické informatiky

Problém stabilních spolubydlících s podmínkami různorodosti spočívá v rozdělení agentů dvou typů do koalic pevné velikosti na základě jejich preferencí, které závisí pouze na počtu agentů stejného typu. V této práci se zabýváme stabilitou takových rozdělení v závislosti na velikosti koalice a struktuře preferenčních profilů agentů. Snažíme se uchopit problém v celé jeho šíři a vytvořit nadhled nad celou problematikou představením Hedonických her a jejich zajímavých podtříd. Představujeme nový randomizovaný algoritmus na rychlé hledání core stabilních řešení instancí tohoto problému a ukazujeme, jakých výsledků jsme pomocí algoritmu dosáhli. Nalezli jsme malou single-peaked instanci s prázdným core a ověřili jsme, že každá instance tohoto problému, kde velikost koalic = 3, preferenční relace všech agentů jsou single-peaked a počet agentů <= 30, velikost koalic = 3 a počet agentů <= 15, velikost koalic = 4, preferenční relace všech agentů jsou single-peaked a počet agentů = 8, má core stabilní řešení. Předkládáme argumenty, proč se domníváme, že každá instance, kde velikost koalic = 3, velikost koalic = 4 a preferenční relace všech agentů jsou single-peaked, má core stabilní řešení.

Práce na DSpace

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

Ing. Šimon Schierreich

Katedra teoretické informatiky

Target Set Selection je NP-těžký problém klíčový v oblasti virálního marketingu. Pro danou sociální síť se problém Target Set Selection zabývá minimální velikostí množiny agentů, jejichž působení nakonec ovlivní každého v dané sociální síti. V této práci představujeme Fair Target Set Selection problém, jehož řešení uspokojuje férovou cenu. Férová cena vynucuje férové rozdělovení target setu omezením maximalního počtu agentů v okolí nějakého agenta v řešení. V této práci studujeme parametrizovanou složitost Fair Target Set Selection a ukazujeme jeho W[1]-těžkost vůči parametrům treewidth, feedback vertex set number a treedepth, W[2]-těžkost pro jeho přirozený parametr férovou cenu. Jako pozitivní výsledek ukazujeme FPT algoritmus při parametrizeci kombinovaným paremetrem vertex cover number a férová cena. Naše další výsledky se dostavují při zohlednění speciálních případů thresholdové funkce. Dokazujeme NP-těžkost pro Fair Target Set Selection a to i tehdy, když jsou všechny thresholdy rovny konstantě c >= 3. Na závěr předkládáme argumenty, proč se domníváme, že Fair Target Set Selection s majoritními tresholdy lze řešit na stromech v polynomiálním čase.

Práce na DSpace

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

prof. Ing. Pavel Tvrdík, CSc.

Katedra počítačových systémů

Tato práce se zabývá úvodem do procesu deduktivní formální verifikace. Teoretická část práce seznámí čtenáře s frameworkem Frama-C pro modulární analýzu programů napsaných v jazyce C. Ten k verifikaci používá pluginy, automatické systémy pro dokazování teorémů a anotační jazyk ACSL. Dále jsou rozebrány důležité části verifikačního prostředí, jeho instalace a použití. Praktická část blíže seznámí čtenáře na ukázkových příkladech s použitými taktikami a metodami. Výsledkem práce je plně verifikovaný algoritmus pro hledání minimální kostry v grafu.

Práce na DSpace

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

RNDr. Radek Hušek, Ph.D.

Katedra teoretické informatiky

Tato práce popisuje implementaci binární minimové haldy a formální důkazy korektnosti jednotlivých operací. Ověřená binární halda je následně použita v Dijkstrově algoritmu pro hledání nejkratší cesty v grafu.

Práce na DSpace

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

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

Katedra teoretické informatiky

Přiřazovací problém je problémem na pomezí matematické a ekonomické teorie. Přiřazovací problém se skládá z agentů a položek, agenti vyjadřují své preference k položkám a cílem je najít (určitým způsobem) optimální přiřazení. Problém přiřazení je velmi dynamický problém, protože může být vzato v úvahu mnoho dalších aspektů. V tomto příkladu mají agenti více seznamů preferencí, jak je předesláno v Parameterized Analysis of Assignment Under Multiple Preferences. My jsme však k problému přistoupili jinak než v článku, motivováni množstvím výzkumů, které již byly provedeny v oblasti problému přiřazení jednoho preferenčního profilu, uvádíme syntézu jednoho profilu z více profilů. Stejně jako představení algoritmu pro nalezení Pareto optimálního řešení na takových profilech. Vzhledem k tomu, že námi prezentované profily umožňují rovnost mezi dvěma položkami (což znamená, že žádná z nich není preferována před druhou), museli jsme zvolit poněkud odlišný přístup. Hlavním cílem bylo najít algoritmické řešení se složitostí alespoň v polynomiálním čase, což se podařilo. Zabýváme se také různými aspekty spravedlnosti při takovém zadání. Následující řešení by měla být přínosná nejen pro Přiřazovací problém s více preferencemi, neboť představují nový pohled na nedávno publikovaný problém, ale také pro Přiřazovací problém s nestriktními profily.

Práce na DSpace

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

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

Katedra počítačových systémů

Union-Find je dátová štruktúra používaná v úlohách, ktoré vyžadujú množinovú operáciu zjednotenia a identifikáciu, do akej množiny prvok patrí. Programátori často tieto štruktúry neimplementujú sami, ale vyhľadávajú ich implementácie online. V takom prípade je problémom overenie, že implementácia funguje správne a že vykonáva iba to čo má. Táto práca sa preto zameriava na analýzu dátovej štruktúry Union-Find, možnosťami jej implementácie, verifikáciou a porovnaním výkonnosti jednotlivých implementácií.

Práce na DSpace

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

Ing. Jiří Smítka

Katedra počítačových systémů

Tato práce se zabývá zjišťováním možností formální deduktivní verifikace šifrovacího algoritmu RSA. Teoretická část čtenáře uvede do problematiky formální deduktivní verifikace, představí její základní koncepty a nastíní její současné průmyslové využití. Dále je představen samotný algoritmus RSA a verifikační prostředí Frama-C určené pro programy v jazyce C, které využívá anotací a automatických systémů k dokazování teorémů. Praktická část se zabývá praktickou ukázkou využití konceptů nastiněných v teoretické části pomocí demonstrační implementace algoritmu RSA v jazyce C a jejího částečného ověření pomocí Frama-C a anotačního jazyka E-ACSL. Výsledkem práce je částečně verifikovaná implementace šifrovacího algoritmu RSA. Jeden z praktických přínosů verifikace je pak demonstrován pomocí zastavení ukázkového SO/DLL injection útoku na jednu z komponent této implementace.

Práce na DSpace

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

Mgr. Michal Opler, Ph.D.

Katedra teoretické informatiky

Tato práce se zabývá hledáním vítěze ve volbách komisí. Poskytujeme přehled volebních systémů pro single-winner a multi-winner volby. Hledání vítěze je často výpočetně náročné, proto zavádíme volby se strukturovanými preferencemi. Ve volbách se strukturovanými preferencemi jsou hlasy voličů nějakým způsobem omezené, což může usnadnit vytváření efektivnějších algoritmů pro hledání vítěze. Popisujeme některé ze známých strukturovaných preferencí. Poskytujeme přehled současné literatury týkající se strukturovaných a téměř strukturovaných preferencí. Zkoumáme současné práce týkající se volby komisí se strukturovanými preferencemi a použití ordered weighted average (OWA) ve volbách komisí. Představujeme polynomiální algoritmy pro hledání vítězných komisí v approval volbách s OWA vektorem (0, ..., 0, 1) a intervalově omezenými voličskými preferencemi. V takových volbách, volič schvaluje komisi pouze pokud schvaluje všechny její členy. Tuto vlastnost používáme a ukazujeme dva přístupy pro hledání výherní komise.

Práce na DSpace

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

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

Katedra teoretické informatiky

Práce se věnuje Hedonickým hrám a přináší přehled používaných konceptů stability a omezení preferenčních profilů. Dále se zaměřuje na upravenou verzi Hedonických her, při které se z existující struktury koalic tvoří nová, protože došlo ke změně množiny agentů odchodem části původních a příchodem stejného počtu nových. Omezuje se na doplnění nových agentů na místa, která část původních opustila, a to v rámci anonymních Hedonických her. Pro tento případ byl vytvořen polynomiální algoritmus pro nalezení striktně core stabilní struktury koalic, navržen pomalý algoritmus pro core stabilní strukturu koalic a pro ni bylo také popsáno několik způsobů převodu na toky v sítích.

Práce na DSpace

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

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

Katedra počítačových systémů

Tato práce se zabývá implementaci Dinitzova algoritmu pro hledání maximálního toku v síti a formálnímu důkazu jednotlivých použitích funkcí. Teoretická část seznámí čtenáře s teorií toků v sítích a myšlenkou Dinitzova algoritmu. Představí čtenáři také framework Frama-C pro formální analýzu kódu v programovacím jazyce C a anotační jazyk ACSL, který frameworku pomáhá s verifikací. Praktická část seznámí čtenáře s použitými metodami pro implementaci Dinitzova algoritmu a také objasní použité anotace pro verifikaci algoritmu.

Práce na DSpace

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

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

Katedra teoretické informatiky

V této bakalářské práci představujeme a zkoumáme problém Multi-Graph Multi-Constrained Optimal Path (MGMCOP). Tento problém souvisi s problémem obchodniho cestujiciho (TSP), který je známý jako NP-úplný problém. Problém MGMCOP má široké uplatněni v různých reálných scénářich, zejména v řidkých sitich, kde je výpočetni efektivita velmi důležitá. Představujeme algoritmus dynamického programováni, který pro řešeni tohoto problému posky- tuje pseudo-polynomiálni časovou složitost. Nicméně, hlavni část naši práci se týká uplatněni konkrétnich omezeni na vstupni data. Tato omezeni, pečlivě navržená a implementovaná, snižuji časovou složitost našeho algoritmu na polynomiálni. Toto sniženi složitosti je dosaženo bez obětováni přesnosti řešeni a praktické užitnosti v řidkých sitich.

Práce na DSpace

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

Ing. Daniel Vašata, Ph.D.

Katedra aplikované matematiky

Maps of elections je framework, který umožňuje vizualizovat a analyzovat sady volebních datasetů. Dosud bylo možné pracovat pouze s datasety, ve kterých měly všechny volby stejný počet kandidátů. V této práci framework rozšiřujeme o možnost současného zpracování datasetů s různými počty kandidátů. Toho dosahujeme jednak rozšířením již existující positionwise metriky, a dále zavedením a implementací tzv. feature metriky. Tyto metriky testujeme pomocí syntetických dat generovaných balíčkem Mapel.

Práce na DSpace

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

Ing. Jan Matoušek

Katedra softwarového inženýrství

Cílem bakalářské práce je vytvoření webového provozního deníku kompresoru. Tato webová aplikace nabízí evidenci kompresorů, tlakových lahví, plnění tlakových lahví a dalších prostředků jednotek sborů dobrovolných hasičů. Nad rámec nabízí také základní evidenci revizí prostředků, jejich umístění a použití hasiči. Jednotlivé záznamy jsou zabezpečeny podle rolí hasiče, který je povinen se do aplikace řádně přihlásit. Rozhraní aplikace je přístupné z mobilního zařízení. Pro její implementaci byly použity technologie nenáročné na běžné hostování. Aplikace je rozdělená na prezentační vrstvu napsanou v Reactu a logickou vrstvu napsanou v Symfony.

Práce na DSpace

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

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

Katedra teoretické informatiky

Tato práce shrnuje známé výsledky problému Equitable Connected Partition a zavádí nový kernelizační algoritmus dokazující, že ECP připouští jádro o velikosti $2^{O(k^2)} \cdot n^{O(1)}$, když je parametrizováno krycí číslo vrcholu ($k$) vstupního grafu G

Práce na DSpace

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

Mgr. Martin Jureček, Ph.D.

Katedra informační bezpečnosti

Tato práce se zabývá využitím formální verifikace pro zajištění bezpečnosti a správnosti implementace Dijkstrova algoritmu. Text je strukturován na sedm kapitol, které seznámí čtenáře s teorií grafů, problémemnejkratší cesty, Hoarovou logikou a frameworkem Frama-c, který slouží k analýze programů napsaných v jazyce C. Dále tento text vysvětlí využití interních pluginů na formální ověření a také jak správně přidat anotace ze specifikačního jazyka ANSI/ISO do zdrojového kódu. Výsledek této práce je ověřená implementace Dijkstrova algoritmu řešící problém nejkratší cesty z jednoho zdroje.

Práce na DSpace

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

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

Katedra teoretické informatiky

V teto praci se zabyvame problemem minimalizace celkove spotreby energie bezdratove site, ktery je formalne znamy jako Min-Power Symmetric Connectivity. Modelem bezdratove site je hranove ohodnoceny neorientovany graf. Cilem je najit souvisly podgraf, ktery pokryva vsechny vrcholy, s minimalnim souctem cen vsech vrcholu. Cena vrcholu je dana nejvetsi vahou hrany incidentni s danym vrcholem. Je znamo, ze se jedna o NP-tezky problem. Toto tvrzeni rozsirime a ukazeme, ze problem je NP-tezky pro konkretni tridu uplnych grafu. Dale predstavime dva postupy umoznujici efektivnejsi reseni Min-Power Symmetric Connectivity problemu. Jedna z metod se zameruje na hledani tzv. povinneho podgrafu. Ten jsme schopni efektivne nalezt za pomoci dolnich mezi cen vrcholu. Predstavime metodu, jak tyto dolni meze cen vrcholu zvysit. Dale se zabyvame moznou redukci poctu hran. Ukazeme metodu identifikujici nadbytecne hrany grafu, cimz snizime vypocetni slozitost ulohy.

Práce na DSpace

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

Ing. Daniel Vašata, Ph.D.

Katedra aplikované matematiky

V této práci se zabýváme problémem víceagentního prohledávání, kde skupina spolupracujících agentů má za úkol společně prohledat v co nejkratším čase dané prostředí, jehož podobu a priori neznají. V simulacích zkoumáme, jaký má změna vzdálenosti, na kterou agenti mohou během prohledávání komunikovat, vliv na celkový čas prohledávání. Toto přesněji zkoumáme na algoritmu, který využívá funkci obsazenosti, díky které se agenti snaží v daný moment vybrat vzájemně vzdálené cílové pozice. Dále studujeme také vliv asymetrické komunikace mezi agenty, jež je simulována za využití Poissonova rozdělení. Zabýváme se také tím, zda se v prohledávání projeví Paretův princip, kdy pouze malá podmnožina agentů prohledala podstatnou většinu území. Prostředí ve kterém se agenti nachází je reprezentováno jako mřížkový graf. Pro experimenty implementujeme simulátor, do kterého je případně možné zakomponovat i jiné strategie prohledávání.

Práce na DSpace

RNDr. Dušan Knop, Ph.D.

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

Katedra teoretické informatiky

Neorientovany graf G=(V,E) nazveme součtovym grafem, pokud existuje injektivni funkce s: V - N přiřazujici vrcholům kladna cela čisla tak, že pro každe dva vrcholy u,v [?] V plati, že jsou v grafu G spojeny hranou pravě tehdy, když existuje třeti vrchol w [?] V takovy, že s(w) = s(u) + s(v). Neni těžke nahlednout, že žadny souvisly graf nemůže byt součtovym grafem, jelikož vrchol s největšim priřazenym čislem nemůže mit žadneho souseda. Proto se snažime najit součtove čislo grafu G, což je minimalni počet izolovanych vrcholů, ktere je třeba ke grafu G připojit, abychom z něj součtovy graf udělali. Zminěny problem studujeme v cele jeho šíři. Nejdřive se věnujeme formalnimu zavedeni všech pojmů a studiu vlastnosti součtovych grafů. Pro vybrane třidy grafů pak uvadime deterministicke algoritmy, ktere z grafu G vytvoři součtovy graf za použiti minimalniho možneho počtu přidanych vrcholů. V posledni časti prace prezentujeme naš exaktni exponencialni algoritmus, ktery dokaže najit součtove čislo libovolneho grafu.

Práce na DSpace

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

RNDr. Petr Olšák

Katedra aplikované matematiky

V dynamicky se měnícím světě nemůžeme očekávat, že naše preference zůstanou neměnné pod vlivem vnějších faktorů. Proto potřebujeme, aby se řešení našich problémů dobře adaptovaly těmto změnám. V problému \textsc{Stable Marriage} se skupiny mužů a žen párují podle jejich \textit{preferencí}. Cílem je najít takové párování, kde neexistuje muž a žena, kteří se vzájemně preferují před svými aktuálními partnery. Efekt dynamicky se měnících preferencí těchto žen a mužů studujeme v rámci naší definice problému jako \textsc{Temporal Stable Marriage}, který tyto změny řeší. Řešením tohoto problému je nalézt párování, ve kterém se nejvýše \textit{k} párů preferuje vzájemně před jejich přiřazenými partnery pod více preferenčními profily. Dokazujeme, že tento problém je \textit{NP-úplný}, i s konstantní hodnotou \textit{k}, a navrhujeme algoritmy, které jsou potencionálně už jen pár pozorování vzdálené od schopnosti vracet správné řešení v čase lepším, než naivní algoritmus hrubou silou.

Práce na DSpace

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

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

Katedra teoretické informatiky

Mikroagregace je technika sloužící k rozdělení dat do shluků dle zadaných velikostních a vzdálenostní požadavků. V této práci se zabýváme případem, kdy data tvoří sít a dvěma variantami, zda shluky jsou souvislé nebo nejsou. Problém zkoumáme z hlediska kombinací parametrů danými problémem (maximální velikost shluků, maximální vzdálenost) a strukturálních parametrů (velikost vrcholového pokrytí, stromové šířky, stromové hloubky). Představujeme několik algoritmů, které ukazují, že problém lze efektivně řešit pomocí parametrizované složitosti. Jmenovitě představujeme pro souvislou verzi problému dynamické programování na stromovém rozkladu. Dále při parametrizaci pomocí velikosti vrcholového pokrytí a maximální vzdálenosti do centra ukazujeme FPT algoritmus na bázi celočíselného programování pro obě verze problému. Na druhé straně ukazujeme že problém je W[1] těžký při parametrizaci stromovou hloubkou a maximální vzdáleností v rámci souvislých shluků. Pokud jsou povoleny nesouvislé shluky, je problém W[1] těžký při parametrizaci velikostí vrcholového pokrytí. Nakonec ukazujeme, že problém Equitable Connected Partition je W[1] těžký vzhledem k parametru stromové hloubky.

Práce na DSpace

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

Mgr. Michal Opler, Ph.D.

Katedra teoretické informatiky

V této práci se zabýváme následujícím modelem šíření názoru v sociální síti. Na začátku někteří jedinci přijmou jistý názor (například tak, že jsou uplaceni). Poté se názor v síti šíří v diskrétním smyslu podle následujících pravidel. Jedinec, který ještě tento názor nemá, jej přijme, pokud dostatečné množství jeho přímých sousedů už názor má. Úkolem pak je ovlivnit malé množství jedinců tak, aby názor zaplavil celou síť. Tento model odpovídá notoricky těžkému problému Target Set Selection. V této práci řešíme tento problém v geometricky motivovaných grafových třídách, konkrétně ve třídě unit disk grafů. Ukazujeme, že i pro tuto třídu je problém Target Set Selection NP-těžký i když má vstupní graf maximální stupeň 4 a~hodnota prahové funkce je nanejvýš 2. Také ukazujeme NP-těžkost v případě, kdy je prahová funkce nastavena na majoritu. Po cestě ukazujeme podobné výsledky pro související třídy grafů jako jsou disk contact grafy nebo mřížkové grafy.

Práce na DSpace