Original title: Konstrukce modelů pomocí CSP
Translated title: Model building using CSP
Authors: Peterová, Alena ; Stanovský, David (advisor) ; Kazda, Alexandr (referee)
Document type: Bachelor's theses
Year: 2011
Language: cze
Abstract: [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.
Keywords: CSP; first-order logic; MACE-style method; MiniZinc; symmetry reduction; CSP; logika 1. řádu; metoda MACE; MiniZinc; redukce symetrií

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/37858

Permalink: http://www.nusl.cz/ntk/nusl-302115


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Bachelor's theses