Strukturované problémy pro SAT
| Název práce v češtině: | Strukturované problémy pro SAT |
|---|---|
| Název v anglickém jazyce: | Structured problems for SAT |
| Klíčová slova: | strukturovaný problém, SAT |
| Klíčová slova anglicky: | structured problems, SAT |
| Akademický rok vypsání: | 2012/2013 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra teoretické informatiky a matematické logiky (32-KTIML) |
| Vedoucí / školitel: | RNDr. Jan Hric |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 18.11.2012 |
| Datum zadání: | 10.12.2012 |
| Datum potvrzení stud. oddělením: | 18.12.2012 |
| Datum a čas obhajoby: | 02.09.2013 00:00 |
| Datum odevzdání elektronické podoby: | 02.08.2013 |
| Datum odevzdání tištěné podoby: | 02.08.2013 |
| Datum proběhlé obhajoby: | 02.09.2013 |
| Oponenti: | RNDr. Petr Kučera, Ph.D. |
| Zásady pro vypracování |
| Cílem práce je navrhnout způsoby pro generování strukturovaných problémů pro SAT a změřit chování SAT solveru na těchto problémech.
Některé problémy budou navrženy tak, aby míra strukturovanosti šla měnit, tj. byla možná kombinace s vhodným náhodně generovaným problémem. Navržené problémy by měli být jak přímo navržené pro SAT, tak převedené z nějaké jiné domény (např. CSP). |
| Seznam odborné literatury |
| S. Russell, P. Norvig: Artificial Intelligence, A Modern Approach, Prentice Hall, Englewood Cliffs, USA, 2003
http://www.satcompetition.org/, SAT competition Pipatsrisawat, K. and Darwiche, A. RSat 2.0: SAT Solver Description. Technical report D153. Automated Reasoning Group, Computer Science Department, University of California, Los Angeles. 2007. http://reasoning.cs.ucla.edu/rsat/papers.html |
| Předběžná náplň práce |
| možné názvy:
1. Generování strukturovaných dat pro SAT 2. Chování SAT na strukturovaných problémech 3+ Strukturované problémy pro SAT |