DPLL algoritmus a výrokové důkazy
| Název práce v jazyce práce (slovenština): | DPLL algoritmus a výrokové důkazy |
|---|---|
| Název práce v češtině: | DPLL algoritmus a výrokové důkazy |
| Název v anglickém jazyce: | DPLL algorithm and propositional proofs |
| Klíčová slova: | splniteľné formuly, SAT, rezolúcia |
| Klíčová slova anglicky: | satisfiable formulas, SAT, resolution |
| Akademický rok vypsání: | 2011/2012 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | slovenština |
| Ústav: | Katedra algebry (32-KA) |
| Vedoucí / školitel: | prof. RNDr. Jan Krajíček, DrSc. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 03.10.2011 |
| Datum zadání: | 03.10.2011 |
| Datum potvrzení stud. oddělením: | 02.12.2011 |
| Datum a čas obhajoby: | 22.06.2012 00:00 |
| Datum odevzdání elektronické podoby: | 25.05.2012 |
| Datum odevzdání tištěné podoby: | 25.05.2012 |
| Datum proběhlé obhajoby: | 22.06.2012 |
| Oponenti: | prof. Mgr. Michal Koucký, Ph.D. |
| Zásady pro vypracování |
| DPLL algortimus je základní algortmus pro rozhodování, je-li
výroková formule splnitelná.Běh algoritmu na konkrétní formuli lze chápat jako výrokový důkaz její nesplnitelnosti a naopak, některé důkazy lze interpretovat jako běh DPLL algoritmu. Předmětem práce je vyložit tento vztah a sestrojit vlastní důkazy nesplnitelnosti několika formulí. |
| Seznam odborné literatury |
| Paul Beame, Richard Karp, Toniann Pitassi, and Michael Saks. The efficiency of resolution and Davis-Putnam procedures. SIAM Journal on Computing, 31(4):1048-1075, 2002. |
| Předběžná náplň práce |
| Nastudovat vztah mezi rozhodováním o splnitelnosti výrokových
formulí a důkazy jejich nesplnitelnosti, a několik důkazů sestrojit. |
| Předběžná náplň práce v anglickém jazyce |
| To learn a relation between deciding propositional satisfiability
of a propositional formula and proofs of its unsatisfiability, and to construct a few proofs. |