|
|
Classes of Boolean Formulae with Effectively Solvable SAT
Vlček, Václav ; Čepek, Ondřej (vedoucí práce) ; Kullmann, Oliver (oponent) ; Savický, Petr (oponent)
Práce studuje třídy booleovkských formulí pro které je problém splnitelnosti řešitelný v polynomiálním čase. Zaměřuje se na třídy založené jednotkové rezoluci; popisuje třídy unit refutation complete formulí, unit propagation complete formulí a specialně se zaměřuje na třídu SLUR. Shrnuje její vlastnosti a poslední výsledky dosažené v této oblasti. Hlavním výsledkem je coNP-úplnost testování zda daná formule patří do třídy SLUR. V závěru je třída SLUR rozvinuta do několika různých hierarchií a jsou studovány jejich vlastnosti a vzájemný vztah vzhledem k inkluzi. Powered by TCPDF (www.tcpdf.org)
|
|
|
Strukturované problémy pro SAT
Klátil, Jan ; Hric, Jan (vedoucí práce) ; Kučera, Petr (oponent)
Název práce: Strukturované problémy pro SAT Autor: Jan Klátil Katedra: Katedra teoretické informatiky a matematické logiky Vedoucí bakalářské práce: RNDr. Jan Hric, Katedra teoretické informatiky a ma- tematické logiky Abstrakt: Práce se zabývá implementací generátoru nestrukturovaných dat CSP modelu RB ve formátu XCSP a implementací několika generátorů strukturova- ných dat ve formátu XCSP a DIMACS, za kterými stojí problémy umisťování N-královen, hledání Hamiltonovského cyklu a rozdělování množiny čísel do v sou- čtu stejných podmnožin. Pomocí délek běhů SAT řešiče RSAT pak porovnáváme data získaná pomocí stejného problému přímo ve formátu DIMACS a převede- ním z formátu XCSP. Dalším srovnáním podrobujeme data vynuceně splnitelná a nesplnitelná a spojování dat strukturovaných a nestrukturovaných na úrovni formátu XCSP. Klíčová slova: strukturovaný problém, SAT 1
|
|
|
Plánovací algoritmy a simulace plánu v logistické doméně
Štefan, Zdeněk ; Toropila, Daniel (vedoucí práce) ; Valla, Tomáš (oponent)
Bakalářská práce se zabývá porovnáním některých technik pro řešení plánování v logistické doméně. Její cílem je porovnání schopností těchto technik z umělé inteligence řešit zadaný problém z hlediska optimality nejen mezi sebou, ale i s plány navrženými lidmi. Protože ne všechny plánovače vrací paralelní plány, je potřeba tyto plány paralelizovat. Práce ukazuje, že některé algoritmy dosahují dobré výsledky ve srovnání s lidskými plány, bohužel však kvůli časové a paměťové náročnosti nemůžou být v dnešní době běžně používány pro řešení náročnějších úkolů.
|
|
|
DPLL algorithm and propositional proofs
Hrnčiar, Maroš ; Krajíček, Jan (vedoucí práce) ; Koucký, Michal (oponent)
Dôkazová zložitosť je zaujímavá súčasť matematiky nachádzajúca sa na pomedzí obrovskej oblasti logiky a teórie zložitosti. Skúma aké dôkazové systémy sú potrebné na efektívne dokazovanie rôznych matematických tvrdení. Predmetom tejto práce je spojenie medzi dôkazovými systémami a algoritmami na SAT. Uvidíme, že beh algoritmu na nesplniteľnej formule môže byť nahliadnutý ako výrokový dôkaz jej nesplniteľnosti, čím samotný algoritmus prakticky definuje celý dôkazový systém. Práca je určená najmä čitateľom so záujmom o dôkazovú zložitosť, ale dokáže aj samostatne objasniť princíp rezolúcie, či ponúknuť menej obvyklý pohľad na SAT, no zároveň predpokladá čitateľovu znalosť základov výrokovej logiky, teórie grafov a zložitosti.
|
|
|
Knihovna pro detekci kolizí
Chlubna, Tomáš ; Španěl, Michal (oponent) ; Polok, Lukáš (vedoucí práce)
Tato práce řeší problém detekce kolizí netriviálních polygonálních modelů v trojrozměrném prostoru. Obecně existují postupy, jak tyto kolize matematicky vyjádřit a vypočítat. Pro použití v oblasti informačních technologií jsou však takové metody často nepoužitelné z hlediska výkonu a paměťové náročnosti. Také oproti reálnému světu je třeba pracovat s diskrétním časem, což vede k nutnosti implementace algoritmů, schopných nejen kolize detekovat v daném časovém okamžiku, ale také je předvídat podle dostupných informací o pohybu objektů ve scéně. Návrh řešení vychází zejména z technik používaných v odvětví herního vývoje a fyzikálních simulací. V práci jsou tedy zahrnuty i mechanismy pro optimalizaci, reprezentaci scény a její vykreslování s využitím grafické karty.
|
|
|
SAT Solver akcelerovaný pomocí GPU
Izrael, Petr ; Šimek, Václav (oponent) ; Jaroš, Jiří (vedoucí práce)
Práce se zabývá návrhem a implementací kompletního SAT solveru akcelerovaného na GPU. V první části práce je popsána architektura grafických karet a možnosti platformy CUDA. Následuje popis algoritmů a technik pro řešení problému booleovské splnitelnosti (SAT problému). Je představena zejména rodina kompletních algoritmů založených na DPLL. Právě varianta DPLL, známa jako 3SAT-DC je kompletně převedena na GPU. Práce popisuje problémy s tímto převodem spojené, stejně jako několik optimalizací a analýz. Velkým problémem je nemožnost využít v paralelním prostředí mnohé sofistikované metody známé ze sekvenčních solverů. Řešení bylo porovnáno s obdobným algoritmem implementovaným pro CPU a bylo ukázáno, že může být až 21x rychlejší. Uvedeny jsou i návrhy, jak algoritmus dále rozšířit a akcelerovat.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Magnetická pole pro biomedicínské experimenty
Otýpka, Jan ; Cipín, Radoslav (oponent) ; Patočka, Miroslav (vedoucí práce)
V práci se zabývám řešením magnetických polí pro využití v oboru biomedicíny. Toto řešení zahrnuje volbu správného geometrického uspořádání cívky pro generování magnetického pole s homogenním rozložením magnetické indukce v co největším možném prostoru. V práci jsou srovnány tři typy cívek tj. solenoid, toroid a Helmholtzovou cívkou. U Helmholtzovy cívky a solenoidu je pak provedený rozbor magnetické indukce ve vnitřním prostoru cívek. Další část je věnována elektrické rezonanci v LC obvodu. Ta je potom využitá pro vznik pulsního magnetického pole v Helmholtzově cívce. Jsou zde shrnuty teoretické a praktické poznatky pro návrh a konstrukci rezonančního měniče. Konec je pak věnován měření obvodových veličin a ověření teoretických poznatků.
|
|
| |
|
|
Vliv vakcinace slinami klíštěte \kur{Ixodes ricinus} na přenos \kur{Borrelia burgdorferi} a cytokinový profil hostitele
GREGOROVÁ, Eva
Klíště Ixodes ricinus je jedním z nejvýznamnějších přenašečů patogenů napadajících člověka jako jsou spirochety Borrelia burgdorferi a virus TBE. V této práci byl studován vliv opakovaného sání neinfikovaných nymf I. ricinus a vliv vakcinace slinami klíštěte I. ricinus na přenos Borrelia burgdorferi a produkci cytokinů. Regionální lymfatické uzliny myší C3H/HeN byly vyšetřovány na produkci IL-2, IFN-? a IL-10 imunoenzymatickou metodou ELISA. Množství spirochet v kůži, srdci a močovém měchýři bylo stanovováno kvantitativní PCR v reálném čase.
|
host ::
RSS.