Třídy Booleovských formulí s efektivně řešitelným SATem.
| Název práce v češtině: | Třídy Booleovských formulí s efektivně řešitelným SATem. |
|---|---|
| Název v anglickém jazyce: | Classes of Boolean Formulae with effectively soluable SAT. |
| Klíčová slova: | splnitelnost, třídy booleovských formulí, SAT |
| Klíčová slova anglicky: | satisfiability, classes of boolean formulae, SAT |
| Akademický rok vypsání: | 2013/2014 |
| Typ práce: | rigorózní práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra teoretické informatiky a matematické logiky (32-KTIML) |
| Vedoucí / školitel: | |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 19.12.2013 |
| Datum zadání: | 19.12.2013 |
| Datum potvrzení stud. oddělením: | 19.12.2013 |
| Datum a čas obhajoby: | 09.04.2014 00:00 |
| Datum odevzdání elektronické podoby: | 19.12.2013 |
| Datum odevzdání tištěné podoby: | 19.12.2013 |
| Datum proběhlé obhajoby: | 09.04.2014 |
| Zásady pro vypracování |
| Úkolem diplomanta je zpracovat přehled výsledků o třídách Booleovských formulí, pro které je problem splnitelnosti (SAT) řešitelný v polynomiálním čase, a pokusit se zjistit vzájemné vztahy těchto tříd (vzhledem k inkluzi) pro dvojice tříd u kterých tento vztah není znám, případně odvodit další zajímavé výsledky o těchto třídách. |
| Seznam odborné literatury |
| Boolean Functions and Computation Models
Clote, Peter; Kranakis, Evangelos Springer Verlag 2002 ISBN: 3-540-59436-1 Boolean Functions : Theory, Algorithms, and Applications Crama, Yves; Hammer, Peter L. dosud nepublikovaný obsáhlý manuskript dostupný na http://www.rogp.hec.ulg.ac.be/Crama/Publications/BookPage.html |
| Předběžná náplň práce |
| Problém splnitelnosti Booleovských formulí (SAT) je jedním z nejznámějších výpočetně těžkých problémů v teoretické informatice. Velkou praktickou důležitost proto mají třídy formulí, pro které je SAT řešitelný v polynomiálním čase. Práce se zabývá zkoumáním právě těchto tříd. |