DPLL algoritmus a výrokové důkazy
| Thesis title in thesis language (Slovak): | DPLL algoritmus a výrokové důkazy |
|---|---|
| Thesis title in Czech: | DPLL algoritmus a výrokové důkazy |
| Thesis title in English: | DPLL algorithm and propositional proofs |
| Key words: | splniteľné formuly, SAT, rezolúcia |
| English key words: | satisfiable formulas, SAT, resolution |
| Academic year of topic announcement: | 2011/2012 |
| Thesis type: | Bachelor's thesis |
| Thesis language: | slovenština |
| Department: | Department of Algebra (32-KA) |
| Supervisor: | prof. RNDr. Jan Krajíček, DrSc. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 03.10.2011 |
| Date of assignment: | 03.10.2011 |
| Confirmed by Study dept. on: | 02.12.2011 |
| Date and time of defence: | 22.06.2012 00:00 |
| Date of electronic submission: | 25.05.2012 |
| Date of submission of printed version: | 25.05.2012 |
| Date of proceeded defence: | 22.06.2012 |
| Opponents: | prof. Mgr. Michal Koucký, Ph.D. |
| Guidelines |
| 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í. |
| References |
| 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. |
| Preliminary scope of work |
| Nastudovat vztah mezi rozhodováním o splnitelnosti výrokových
formulí a důkazy jejich nesplnitelnosti, a několik důkazů sestrojit. |
| Preliminary scope of work in English |
| To learn a relation between deciding propositional satisfiability
of a propositional formula and proofs of its unsatisfiability, and to construct a few proofs. |