Obtížnost hledání min

Snad každý, kdo kdy používal Windows, zná hru Minesweeper, tedy hledání min. Různé hry, včetně této, se staly předmětem seriózního teoretického výzkumu. Například bylo zjištěno, že Sokoban (skladník přesouvající bedny na určené místo) je NP-těžký problém. Stejně tak hledání min je NP-těžké. Zde jako malé myšlenkové cvičení ukázka, jak lze algoritmicky řešit hledání min převedením na problém splnitelnosti výrokových formulí (SAT).

Předpokládám, že čtenář zná pravidla hry. Nejprve je nutné rozhodnout se pro formální reprezentaci stavu hry. Každý element hrací plochy buď obsahuje minu, nebo ne. Již odhalená nezaminovaná pole mají číslo, jež udává počet min na sousedních polích (včetně diagonálních, tj. rohové pole má tři sousedy, pole na okraji mimo roh pět a pole někde uprostřed osm). Mějme tedy atomické predikáty numbered(x,y,z), mined(x,y) a safe(x,y). Predikát numbered říká, že na pozici [x,y] je číslo z, mined říká, že na dané pozici je určitě mina a safe, že tam určitě mina není.

V každém momentu hry můžeme její stav zakódovat pomocí uvedených predikátů. Zbývá určit vztahy mezi predikáty, tedy axiomy, které jsou vždy splněny. Platí, že pokud je v nějakém poli číslo, určitě tam není mina (a naopak):

∀x.[∃z.numbered(x,y,z)≡safe(x,y)]

Dále víme, že zaminovanost určité pozice a její bezpečnost se vylučují:

∀x.∀y.¬[mined(x,y) & safe(x,y)]

A nakonec dáme smysl číslu na určité pozici:

∀x.∀y.∀z.numbered(x,y,z)≡:ne­ighbour(u,v,x,y) & mined(u,v)|=z & |[u,v]:neighbour(u,v,x,y) & safe(u,v)|=|[u,v]:neighbou­r(u,v,x,y)|-z]

Jinými slovy, počet určitě zaminovaných polí kolem [x,y] je z a počet určitě nezaminovaných je počet sousedů bez z (použili jsme pomocný predikát neighbour se zřejmým významem).

Umíme tedy formálně zakódovat stav hry. A jak ji řešit? Máme-li již výše popsanou logickou reprezentace, není nic snazšího než převést všechny relevantní formule na výrokovou logiku. Druhý axiom například bude ¬mined(x,y) ⋁ ¬safe(x,y) pro všechna x a y. A tak dále.

Získané výrokové formule dáme k řešení libovolnému SAT solveru. Moderní solvery umí efektivně řešit problémy se statisíci výrokových proměnných, my jich při hledání min (v závislosti na velikosti hrací plochy) budeme mít tisíce, takže řešení vždy dostaneme ve zlomku sekundy (a řádově rychleji by to vzhledem k NP-úplnosti problému hledání min ani nešlo).

Zbývá dekódovat řešení. Především je třeba si uvědomit, že řešení může být více (pokud je situace nejednoznačná). Pokud pro nějaké pole platí mined, určitě tam je mina. Pokud platí safe, mina tam určitě není. Zároveň díky axiomatizaci platit nemůžou a pokud neplatí ani jedno, za dané situace nevíme, nachází-li se tam mina nebo ne.

Kdo by si chtěl výše popsaný algoritmus vyzkoušet, může v C(++) použít například solver Minisat, v Javě třeba SAT4J.