Název: Efektivní zakódování hlavolamů Hidato a Numbrix do jejich CNF reprezentace
Překlad názvu: Effective encoding of the Hidato and Numbrix puzzles to their CNF representation
Autoři: Bartoš, Samuel ; Balyo, Tomáš (vedoucí práce) ; Vodrážka, Jindřich (oponent)
Typ dokumentu: Bakalářské práce
Rok: 2014
Jazyk: eng
Abstrakt: [eng] [cze]
Although Boolean satisfiability problem (SAT) is NP-complete, thanks to the progress in the performance of SAT solvers many other problems can be solved efficiently by encoding them into Boolean formulas. In this thesis this method is applied to find the solution to Hidato and Numbrix puzzles. We present various encoding techniques and describe an implementation of an application designed to construct them. The efficiency of individual encodings together with their effect on the performance of several SAT solvers is examined. The results of conducted experiments indicate that the efficiency of encoding can change from solver to solver and that the best choice of encoding-solver combination depends heavily on the size and type of puzzle. Powered by TCPDF (www.tcpdf.org) I když je problém booleovské splnitelnosti NP-úplný, díky pokroku výkonnosti SAT solverů, může být mnoho jiných problémů řešeno efektivně, když je zakódujeme do booleovkých formulí. V této práci je tato metoda použita k nalezení řešení hlavolamů Hidato a Numbrix. Ukázáno je několik kódovacích technik spolu s implementací aplikace, která je sestrojuje. Zkoumáme také efektivitu jednotlivých kódování i jejich vliv na výkon různých SAT solverů. Výsledky experimentů ukazují, že efektivita kódování se u různých solverů může lišit a také že výběr nejlepší kombinace solver-kódovaní závisí na velikosti a typu hlavolamu. Powered by TCPDF (www.tcpdf.org)
Klíčová slova: Hidato; kódování; Numbrix; SAT; encoding; Hidato; Numbrix; SAT

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/63776

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


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