|
|
Simulace a optimalizace metod DNA výpočtů
Plevač, Lukáš ; Zachariášová, Marcela (oponent) ; Bidlo, Michal (vedoucí práce)
Tato práce se zaměřuje na vytvoření programu pro simulaci architektury výpočtů SIMD||DNA a následné využití této simulace k navrhování nových algoritmů pro tuto architekturu, jako jsou například posuvný registr, 3-Stavový celulární automat nebo LFSR registr. SIMD||DNA patří mezi výpočetní architektury v oblasti DNA výpočtů, což je netradiční způsob výpočtů zcela odlišný od dnešních elektronických počítačů. Hlavním principem DNA výpočtů je využití vlastností DNA pro zpracování informací. Tato metoda přináší výhody v energetické efektivitě a masivním paralelismu teoreticky umožňujícím překonat současné limity zpracování informací. Taktéž nabízí vyšší hustotu ukládání informací, což vedlo k vzniku nového typu úložišť známých jako DNA digital data storage. SIMD||DNA je architekturou, která se snaží provádět výpočty s takto uloženými daty.
|
|
|
Simulace pevných těles
Leitner, Denis ; Milet, Tomáš (oponent) ; Chlubna, Tomáš (vedoucí práce)
Táto práca je zameraná na simuláciu fyziky pevných telies v reálnom čase. Popisuje základné postupy používané pri hernom vývoji zamerané na detekciu kolízie medzi konvexnými mnohostenmi. Ďalej popisuje riešenie zistenej kolízie a spôsob simulácie dynamiky pevných telies. Zaoberá sa takisto aj návrhom a implementáciou simulátoru pevných telies v jazyku C++. Na vykresľovanie scény je použité OpenGL.
|
|
|
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.
|
|
|
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.
|
|
| |
|
|
Vizualizace hmatových a zvukových vjemů
Lukš, Roman ; Zachariáš, Michal (oponent) ; Polok, Lukáš (vedoucí práce)
Cílem této bakalářské práce je návrh a implementace vizualizace hmatových a zvukových vjemů běžících v reálném čase. Vjemy mají sloužit pro orientaci hráče v jednoduché 2D hře místo zraku. Vjemy jsou vizualizovány pomocí shaderů na GPU. Zvukové vjemy jsou implementací simulace vlnění výpočetně nenáročnou explicitní metodou. Hmatový vjem je tvořen pomocí pohyblivých čar. K vykreslování je použita knihovna OpenGL. V práci jsem vytvořil funkční herní prototyp obsahující dvojici vjemů.
|
|
|
Využití SAT solverů v úloze optimalizace kombinačních obvodů
Minařík, Vojtěch ; Mrázek, Vojtěch (oponent) ; Vašíček, Zdeněk (vedoucí práce)
Tato práce zavádí využití řešení problému SAT a jeho modifikací v úloze evolučního návrhu kombinačních obvodů. Motivací využití těchto problémů je zrychlení ohodnocování chromozomů kandidátních řešení fitness funkcí během evoluce v případech, kdy selhává metoda klasické simulace. Využití problému SAT, respektive #SAT umožňuje oproti simulaci zrychlení zejména pro komplikované obvody s velkým počtem vstupů. Implementované řešení se zalkádá právě na problému #SAT. Celkem byly implemenyovány dvě různé varianty využití tohoto problému. Varianty se liší metodou kontorly rozdílných hodnot na výstupech obvodu. Protože implementované řešení využívá k reprezentaci obvodu logickou formuli a zkoumá její splnitelnost, časová složitost algoritmu závisí především na logické složitosti navrhovaného obvodu.
|
|
|
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.
|
|
|
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ů.
|
|
|
Modelování kooperativního hledání cest
Ježek, Milan ; Surynek, Pavel (vedoucí práce) ; Majerech, Vladan (oponent)
V této práci jsou popsány nové modely pro řešení kooperativního hledání cest (cpf) s požadavkem na minimální makespan a je provedeno jejich experimentální porovnání se stávajícími modely. Nové modely uvedené v práci zkoumají možnosti kódování problému cpf pomocí celočíselného lineárního programování s binárními proměnnými (bip) a jako problém splnitelnosti omezujících podmínek (csp). Při testech se ukázaly hlavně poměrně dobré výsledky nového modelu IP active-edges při vyšším množství agentů, kdy jen mírně zaostával za nejlepším SAT modelem. Nový model pro csp dosáhl nejrychlejších časů v testech s nízkým množstvím překážek a interakcí mezi agenty, zatímco v opačném případě se jeho výkon dramaticky snižoval. Powered by TCPDF (www.tcpdf.org)
|
host ::
RSS.