Minesweeper és Tetravex, ipari SAT performance

A legtöbb "lepakolós" kirakójáték (vannak valami objektumok, amiket le kell pakolni egy táblára valamilyen szabályok szerint) NP-beli, hiszen egy lepakolás egy tanúsítvány a konzisztenciára - még egyszer, a konzisztencia kérdés egy eldöntési probléma: kirakójátékoknál a konzisztencia úgy néz ki általában, hogy az eredeti objektumokból már leraktunk párat a táblára, kérdés, hogy be lehet-e fejezni, ahogy elkezdtük. Nyilván ha a konzisztenciára van "jó" algoritmusunk, akkor magára a kirakásra is van: lerakunk egy még nem lerakott objektumot valahova, hívjuk a konzisztenciát. Ha OK, akkor az az objektum ott marad és fogjuk a következőt; ha nem OK, akkor máshova rakjuk és hívjuk a konzisztenciát, amíg egyszer azt nem kapjuk, hogy OK. (Ha sehova nem lehet lerakni, akkor eleve nem volt konzisztens az egész tábla).

A tapasztalat azt mutatja, hogy az "addiktív" kirakók NP-nehezek is.

Ilyen például a(z nxn-es) Sudoku lásd pl itt, az Aknakereső, lásd pl itt, vagy a Tetravex, lásd pl itt.

A sztorihoz hozzátartozik, hogy a Tetravexhez nagyon hasonlító Eternity II (a különbség annyi, hogy lehet forgatni a csempéket) meglehetősen direkt pénzszerzési módszernek bizonyult :)  a feladat annyi, hogy a 256 elemet egy 16x16-os rácsba le kell rakni a szokásos edge-matching szabályokat figyelembe véve (minden él két oldalán ugyanaz a szín legyen). Aki először kirakja, kap kétmillió amerikai dollárt, játék indul, három évet adtak rá.

Meglehetősen biztosra mentek :) persze rengetegen írtak rá programot, változatos módszerekkel branch-and-bound backtrackeket, komplett gridrendszereket állítottak rá, gondolom nekimentek SAT és CSP solverekkel is, meg mindennel, ami csak létezik, de a három év letelt és senki nem tudta kirakni. (Állítólag van megoldás. Nem tudni, mindenesetre az se derült ki, hogy ne lenne. Személy szerint úgy gondolom, hogy tényleg van néhány ezer megoldás: ha túl sok lenne, könnyen beleszaladhatott volna valaki, ha meg túl kevés, akkor a branch-and-bound működhetett volna hatékonyan és azért jöhetett volna ki gyorsan- ez a "szokásos" két véglet.)

Mivel eléggé meg lett reklámozva a játék, készítői eladtak belőle az első héten félmillió darabot, 35 dolláros egységáron (egyébként megvettem én is - mindig érdekelt, hogy mitől nehéz egy nehéz probléma egy-egy példánya, nos, ez tényleg nehéz lett :D ), ebből a tizenhét és félmillióból még akár levonva a reklám- és gyártási költséget is, akár a kétmilliót kifizetve, ha ki kell (nem kellett) is szép pluszban zárhattak a készítők ;)

A Tetravexre és az Aknakeresőre készült már nálam szakdolgozat, akiknek a szerzői

1. csináltak a problémára egy "baseline" bactrack solvert,
2. egy okosított solvert
3. és egy "vezessük vissza a SATra, majd adjuk oda egy SAT solver championnak" solvert, amiről itt írtam,
4. meg egy generátort, ami olyan random feladványokat generált, aminek van megoldása,
5. aztán összemérték a két- vagy háromféle megközelítést, hogy veri-e a SATos megoldás a célirányosan fejlesztett backtracket.

A két dolgozat eltérő eredményre jutott :-) Nevezetesen, a Tetravex esetében a SATos megoldás bitang lassú lett, 3x3-asnál nagyobb táblákkal a glucose már nem bírt el, viszont az Aknakeresőt a minisat rommá gyalázta.

Felmerültek bennem a következő kérdések:

1. Mi okozza ezt a különbséget? Erre egy tippem van is: a Tetravex esetében lényegesen nagyobb formulát kapunk (négyzetes nagyot), mint az aknakeresőhöz képest (lineáris nagyot). Ki kéne tesztelni.
2. Lehetne-e egy másik visszavezetéssel jobb eredményt kapni a Tetravexre? (Két probléma közt nem csak egyetlen inputkonverzió lehet - van is a fejemben egy másik, ami az előzőnél talán kompaktabb és emiatt talán gyorsabb is lehet.)
3. Mit alkotnának itt a CSP solverek? Azok állítólag a számos feltételeket jobban kezelik, mint a CNF-ek.
4. Van-e olyan minta, ami "nehézzé" tesz egy-egy konkrét (Tetravex vagy Aknakereső) feladványt? Nyilván lettek generálva olyan példányok is, melyeket könnyű volt megoldani, attól, hogy a probléma úgy általában véve nehéz, még vannak könnyű feladványok. (Nyugdíjasoknak, rejtvényújságban például)
5. Tudnánk-e írni olyan generátort, mely nehéz példányokat generál?
6. Mi a helyzet azokkal a feladatokkal, melyekről tudjuk, hogy pontosan egy megoldásuk van? (A rejtvények általában ugye ilyenek.) Könnyít ez a helyzeten?

Ha valakit érdekelnek a részletek, mailben kérje el a szakpdogákat nyugodtan, webre azt hiszem, nincs jogom felrakni, meg egyébként is :-) A fenti irányok mindegyike, vagy egy újabb NP-teljes probléma hasonló vizsgálata pedig természetesen engem érdekel.

Egyébként SAT solvereket az iparban még alkalmaztak doksik szerint

• Mercedes gyárban, hogy a rendelt alkatrészekből valóban összeáll-e egy, a specifikációnak megfelelő C osztály (pl egy ilyen feltétel "ha van légkondi, akkor a nagyobb akksi kell bele, kivéve a 2.6-os és a 3.2-es dízelmotorral szerelteket", ilyenből van 952)
• Hardware rendszerek ún. "Bounded Model Checking", korlátozott modellellenőrzésére: a rendszer kielégíti-e a specifikációt az első N lépésben (a "tapasztalat" azt mutatja, hogy ha egy elég nagy lépésszámig biztos jó a rendszer, akkor jó is lesz - ezt persze nem kritikus rendszereknél tesszük)
• Aki több példát szeretne látni, nézzen rá a SAT Competition weblapjára, az industrial trackre :-)

A feladatok mérete nem feltétlenül rémisztő: azt láttuk, hogy legrosszabb esetben már száz változó is kezelhetetlenné fajulhat. Ezzel szemben a SAT versenyen félmillió változós, hétmillió klózos inputtal is bánt el solver (2005-ben, azóta gondolom csak jobbak lettek), hogy lássuk a helyiértékeket, miről beszélünk most.