Konstrukce modelů pomocí CSP
| Thesis title in Czech: | Konstrukce modelů pomocí CSP |
|---|---|
| Thesis title in English: | Model building using CSP |
| Key words: | logika 1. řádu, metoda MACE, CSP, MiniZinc, redukce symetrií |
| English key words: | first-order logic, MACE-style method, CSP, MiniZinc, symmetry reduction |
| Academic year of topic announcement: | 2010/2011 |
| Thesis type: | Bachelor's thesis |
| Thesis language: | čeština |
| Department: | Department of Algebra (32-KA) |
| Supervisor: | doc. RNDr. David Stanovský, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 27.10.2010 |
| Date of assignment: | 27.10.2010 |
| Date and time of defence: | 23.06.2011 00:00 |
| Date of electronic submission: | 26.05.2011 |
| Date of submission of printed version: | 26.05.2011 |
| Date of proceeded defence: | 23.06.2011 |
| Opponents: | RNDr. Alexandr Kazda, Ph.D. |
| Guidelines |
| Problém zní, k dané sadě axiomů v predikátové logice najít (konečný) model.
Nejúspěšnější metodou je v současné době převod této úlohy na SAT (splnitelnost booleovských formulí) a její řešení SAT-solverem, tak jak to dělá např. systém Paradox. Cílem práce je navrhnout a implementovat alternativní metodu, převod do jazyka CSP (constraint satisfaction problem) a řešení pomocí nějakého CSP-solveru. Student prostuduje algoritmus, který používá Paradox, navrhne analogický algoritmus pro převod na CSP, a tento algoritmus implementuje s použitím vhodného state-of-the-art CSP-solveru. Systém bude testován na úlohách z knihovny TPTP a porovnán s ostatními systémy na hledání modelů. |
| References |
| dokumentace systémů Paradox a SEM
MiniZinc, http://www.g12.cs.mu.oz.au/minizinc/ knihovna TPTP, http://www.tptp.org John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge Uni. Press, 2009. |