| Abstrakt: | Pri tvorbe logických hier vo veľkej miere sa používajú počítače, na čo
sa používajú špecializované programy na riešenie daných hier. Žiadúce je,
aby zadania mali práve jedno riešenie, pričom pre hry, ako napríklad sudoku,
hamilton snake, slither link, nonogram, je dokázané, že problém odpovedania
na túto otázku je NP-úplný.
V tejto práci skúmame možnosť aplikácie všeobecných SAT-solverov na
problematiku tvorenia zadaní. Ukazujeme na troch konkrétnych hrách (su-
doku, hamilton snake a chaos), že SAT-solvery nás môžu zbaviť potreby
vývoja špecializovaných algoritmov pre mnohé logické hry.
|
|---|