Original title:
Efektivní zakódování hlavolamů Hidato a Numbrix do jejich CNF reprezentace
Translated title:
Effective encoding of the Hidato and Numbrix puzzles to their CNF representation
Authors:
Bartoš, Samuel ; Balyo, Tomáš (advisor) ; Vodrážka, Jindřich (referee) Document type: Bachelor's theses
Year:
2014
Language:
eng Abstract:
[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)
Keywords:
encoding; Hidato; Numbrix; SAT; Hidato; kódování; Numbrix; SAT
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/63776