Název: Konstrukce modelů pomocí CSP
Překlad názvu: Model building using CSP
Autoři: Peterová, Alena ; Stanovský, David (vedoucí práce) ; Kazda, Alexandr (oponent)
Typ dokumentu: Bakalářské práce
Rok: 2011
Jazyk: cze
Abstrakt: [cze] [eng]
V této práci se věnujeme algoritmům na konstrukci konečných modelů pro množiny axiomů logiky 1. řádu s cílem navrhnout a implementovat novou metodu, založenou na převodu na problém splnitelnosti omezení (CSP). V teoretické části představíme standardní metodu MACE, používající převod úloh na SAT, a pokročilejší techniky zvyšující její efektivitu: dělení klauzulí, definici termů a statickou redukci symetrií. Následuje návrh alternativní metody, která podobným způsobem převádí úlohy na CSP. Nově navrhujeme techniku redukce symetrií i pro binární funkce. Poté popíšeme implementaci alternativní metody pomocí CSP-modelovacího jazyka MiniZinc a CSP-solveru Gecode. Na závěr porovnáme výkonnost vytvořeného nástroje na hledání modelů s nejúspěšnějšími zástupci standardních metod, systémy Paradox a Mace4. In the present work, we study algorithms for building finite models of sets of first-order axioms with the aim of proposing and implementing a new method, based on translation onto constraint satisfaction problem (CSP). In the theoretical part, we describe the standard MACE-style method, based on translating problems onto SAT, and advanced techniques that improve the effectiveness of this method: clause splitting, term definitions and static symmetry reduction. Next, we propose an alternative method, which translates problems onto CSP in a similar way. In addition, we have newly proposed a static symmetry reduction technique for binary functions. Next, we describe an implementation of the alternative method using a CSP-modelling language MiniZinc and a CSP-solver Gecode. Finally, we compare performance of our model finder against state-of-the-art representatives of standard methods, systems Paradox and Mace4.
Klíčová slova: CSP; logika 1. řádu; metoda MACE; MiniZinc; redukce symetrií; CSP; first-order logic; MACE-style method; MiniZinc; symmetry reduction

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/37858

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-302115


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Bakalářské práce