National Repository of Grey Literature 1 records found  Search took 0.00 seconds. 
Effective encoding of the Hidato and Numbrix puzzles to their CNF representation
Bartoš, Samuel ; Balyo, Tomáš (advisor) ; Vodrážka, Jindřich (referee)
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)

Interested in being notified about new results for this query?
Subscribe to the RSS feed.