Tegnapelőtt egy fb poszt alatt volt egy agymenés arról, hogy hogyan lehetne valamelyik részéből a logika kurzusnak játékot csinálni (mert akkor aztán megtanulnák :P ), aminek folyományaképp tegnap estére összedrótoztam ezt. Röviden:
Ha valaki már megcsinálta a logika kurzust, akkor felismerheti, hogy ez nagyon hasonlít a rezolúció nevű módszerre, amivel input konjunktív normálformákról (CNF) tudjuk megmutatni, hogy kielégíthetetlenek. Aki hiányzott: vannak 0/1 értékű logikai változók, ezek a pozitív, negáltjaik a negatív literálok, literálokat vagyolva kapunk klózokat, amiket éselve pedig a CNF-et. Például
Mivel a vagyolás és az éselés is kommutatív, asszociatív és idempotens művelet, a sorrend nem számít, és egy klózon belül hogy egy előforduló literál hányszor szerepel, az se számít. Emiatt reprezentálhatunk egy klózt mint literálok egy halmazát, egy CNF-et meg mint klózok halmazát. A fenti pl
A rezolúciós algoritmusban egy ilyen alakú CNF az input és listát írunk klózokról. Egy klózt kétféle okból vehetünk fel:
Például $\{p,\neg q\}$ és $\{\neg p,\neg q\}$ a $p$-n ütközik, rezolvensük $\{\neg q\}$, aminek $\{q\}$-val a rezolvense a $\Box$ jelű üres klóz. Tehát a példa CNF-ünkből levezethető az üres klóz; a rezolúció helyességi és teljességi tétele azt mondja ki, hogy ez pont akkor történik, ha az input CNF kielégíthetetlen.
So far so good.
A játékban persze a színek megfelelnek egy-egy változónak, a teli karika mondjuk a pozitív literál, az üres karika a negatív literál. Ha a mobba belelövünk és lesz ütköző változó, az kiüti egymást, ez pont egy rezolvensképzés. Ha nincs, akkor simán beleolvad - hát ez ugyan nem volt a rezolúciós szabálykönyvben, de math says ha bevennénk ezt is valid szabálynak, akkor az így kapott rezolúciós variáns is helyes és teljes, szóval miért ne. Ha levezettük az üres klózt, azaz ha kiürül a mob, akkor bizonyítjuk, hogy az input kielégíthetetlen, ez OK.
Volt még az a furán hangzó kitétel, hogy egyszerre két ütköző szín game overt ad; ezt azért kellett bevenni, mert ez annak felelne meg, mintha két változó mentén "egyszerre" rezolválnánk, amit viszont a rezolúciós algoritmus nem enged és okkal nem enged: ha tehetnénk ilyet, akkor olyan esetekben is kijönne az üres klóz, mikor a formula kielégíthető. Pl. a $\{p,q\},\{\neg p,\neg q\}$ input kielégíthető, pl. $p=1,q=0$, de ha szabad lenne két változó mentén egyszerre rezolválni, akkor kijönne belőlük az $\Box$.
Viszont nem szabad, hanem kijönne belőlük rezolvensként vagy a $\{q,\neg q\}$, vagy a $\{p,\neg p\}$. Az ilyeneket (amikben van egy változó is és a negáltja is) triviális klóznak hívják és math says ilyet soha nem érdemes levezetni, ha $\Box$ kijöhet, akkor ilyen nélkül is kijön, legalább ugyanolyan gyorsan. Na ezért tehettem meg, hogy inkább letiltottam azt, hogy egyáltalán próbálkozzanak a userek ilyen esetekben a rezolválással.
Ez a játék viszont egy speciális esete a rezolúciós algoritmusnak, mert
amit input rezolúciónak hívnak és gyengébb, mint a "rendes" módszer, mert pl. a $\{p,q\},\{\neg p,q\},\{p,\neg q\},\{\neg p,q\}$ inputról nem tudjuk ilyen módon megmutatni, hogy kielégíthetetlen: az elején mondjuk kiválasztjuk a $\{p,q\}$ klózt, aztán mondjuk rálövünk $\{\neg p,q\}$-val, marad $\{q\}$, amire mondjuk $\{p,\neg q\}$-val, marad $\{p\}$, amire mondjuk $\{\neg p,\neg q\}$-val, marad $\{\neg q\}$, amire ha rálőhetnénk a már levezetett $\{q\}$-val, kész lennénk, de nem tehetjük, csak a négy eredeti input klózzal rezolválhatunk.
Úgy egyáltalán, mivel az üres klózhoz az kell, hogy két ellentétes polaritású egységklózt rezolváljunk, eleve csak akkor jöhet ki inputrezolúcióval az üres klóz, ha van az inputban egységklóz is.
Hogy könnyebb legyen a vizualizáció, azt találtam ki, hogy legyen egy inputrezolúciós játék, akkor mindig csak egyetlen klózt kell nyilvántartani a listából (hiszen a lista már elhagyott elemeit nem használjuk fel újra, eldobhatjuk őket), az lesz a mob mindig, és fegyvereink az eredeti input klózok. (Itt nem gondoltam bele pl abba, hogy az eredeti mob is része az inputnak, tehát a mobot ellenségként is és fegyverként is fel kéne venni, hogy teljes legyen a párhuzam az input rezolúció és a játék közt, de ez elmaradt. benéztem, na.)
Már "csak" arra volt szükségem, hogy írjak egy generátort, ami megoldható pályákat (azaz: olyan kielégíthetetlen CNF-eket, melyekre van inputrezolúciós cáfolat) készít. Persze mivel nem tudtam, hogy pontosan miket lehet legyőzni inputrezolúcióval, ezértgondolkodtam gugliztam ezt a survey cikket. Ebben (Thm 3.1) azt látjuk, hogy
Ez egyszerűsít kicsit, mert az unit (egység) rezolúció annyi, hogy minden rezolválásnál a két klóz legalább egyike egységklóz kell legyen. Pl. a kedvenc példánk esetében, $\{p,\neg q\},\{\neg p,\neg q\},\{q\}$ először üthetjük $\{p,\neg q\}$-t $\{q\}$-val, kapunk $\{p\}$-t, aztán mondjuk $\{\neg p,\neg q\}$-t is $\{q\}$-val (itt ugye nem kell az utolsó klózt is használni mindenképp), kapjuk $\{\neg p\}$-t, ami $\{p\}$-vel együtt kiadja $\Box$-ot.
Úgy általában is igaz, hogy egységrezolúcióra a következő algoritmus működik:
Ha felveszek egy $n\times k$-s $A$ mátrixot, aminek egy sora egy klóz, egy oszlopa egy változó, és $A_{i,j}$ akkor $0$, ha a $j$. változó nem szerepel az $i$. klózban, $1$, ha pozitívan és $-1$, ha negatívan, akkor pl a fenti inputunk mátrixa így néz ki:
$\left(\begin{array}{rr}-1&-1\\1&-1\\0&1\end{array}\right)$, első sor $\{\neg p,\neg q\}$, második $\{p,\neg q\}$, harmadik $\{q\}$. Nyilván sorokat meg oszlopokat csereberélhetek, mert se a klózok sorrendje nem számít, se az, hogy melyik változót hanyadiknak veszem fel. Sőt, egy oszlopban átválthatom az előjeleket is (ha minden $p$-ből $\neg p$-t csinálok és viszont, akkor ugyanazok lesznek a valid rezolválós lépések és minden ugyanúgy marad, az üres klózban meg nincs $p$, az nem változik). Ezért feltehetem, hogy az egységklóz, akivel először irtom a világot, az utolsó sorban van, jobb oldalán van az $1$-es, a többi mező $0$.
Ha ezzel a klózzal rezolválok végig mindent, akkor a fölötte levő $-1$ elemeket $0$-ra állítom. Egyébként math says ha van $C_1\subsetneq C_2$, tehát egy olyan $C_1$ klóz, aminél egy $C_2$ bővebb klóz is van, akkor $C_2$-t el is dobhatom, mert $C_1$-et használni mindig jobb, mint $C_2$-t. Ezért ha van egy $\{p\}$ egységklózom, akkor feltehetem, hogy nincs $\{p,q\}$, $\{p,\neg q,r\}$ etc klózom, vagyis az egységklóz $1$-ese oszlopában nincs több $1$-es.
Ha tehát az egységklózzal végigrezolválok minden mást, akkor rajta kívül kinullázom az oszlopát. Megint átrendezve a sorokat és az oszlopokat meg az oszlopon belül az előjeleket feltehetem, hogy a második ágyúzós egységklóz az utolsó előtti sorban alakul ki, az $1$-es az utolsó előtti cella. Balra tőle nem nullázott az előző egységklóz, tehát ott eleve $0$-k voltak. Jobbra vagy volt $-1$, vagy nem, de most már nincs. Ezzel is végignullázzuk a fölötte levő $-1$-eket, $1$-es továbbra sincs az oszlopban (mert azt a klózt eldobtuk volna), alatta nem lehetett nemnulla (mert akkor az utsó sor nem lett volna egységklóz). A következő egységklóz az előző, stb; azt kapjuk, hogy egy egységrezolúcióval cáfolható "minimális" CNF mátrixa pont így nézhet ki:
ahol $\star$ lehet $0$ vagy $-1$ minden egyes cellában, aztán ennek a sorai meg oszlopai random sorrendet kapnak, és néhány oszlopnak random inkább vesszük az ellentettjét, ennyi. Még azt is látjuk, hogy ez egy $(n+1)\times n$es mátrix kell legyen, ha $n$ változó van. Ezzel a generálást letudtam: csináltam egy ekkora mátrixot, az "átlóját" feltöltöttem $1$-esekkel, alá nulláztam, fölötte random kaptak $0$ vagy $-1$ értéket a cellák. Arra az egyre figyeltem, hogy fölösleges változó ne legyen és minden $1$-es fölött tényleg legyen $-1$ is (különben mit nulláznék).
A fenti tétel szerint tehát ha ilyen mátrixnak sor-oszlop permutálásával és oszlopok mínusz eggyel szorzásával kirakok egy CNF-et, annak lesz inputrezolúciós cáfolata, ami meg nem így néz ki, annak nem lesz (vagy van benne fölösleges klóz/változó, amit nem akartam). Már csak az volt a kérdés, hogy bármelyik elemet kinevezhetem-e mobnak
mert pl. ha az $\{p,\neg q\}$, $\{\neg p,\neg q\}$, $\{q\}$ inputnál épp a $\{q\}$-t nevezem ki mobnak, arra rálövök pl $\{p,\neg q\}$-val, lesz belőle $\{p\}$, amire rálövök a másikkal, lesz belőle $\{\neg q\}$, de attól meg nem szabadulok többet, mert $q$ pozitívan csak a mobban volt, de onnan már eltűnt. (Ez az az eset, ami nem jutott eszembe, hogy a mobot is fel kéne venni fegyvernek: ha $\{q\}$ fegyver is lenne, akkor itt pl megkapnánk az üres klózt.)
Ekkor eszembe jutott a lineáris és az SLD rezolúció tétele. Mind a kettő, bizony.
A lineáris rezolúció annyit jelent, hogy kiindulunk egy input klózból (ez lesz a bázisklóz) és minden egyes lépésben a legutóbb kapott klózt rezolváljuk valamivel. Nem feltétlen input klózzal, lehet a listáról is választani! Pl. a $\{p,q\}$, $\{\neg p,q\}$, $\{\neg p,\neg q\}$, $\{p,\neg q\}$ inputból kiindulunk $\{p,q\}$-ból, rálövünk a másodikkal, lesz $\{q\}$, arra a harmadikkal, lesz $\{\neg p\}$, arra a negyedikkel, lesz $\{\neg q\}$, és erre a lista második elemével, $\{q\}$-val lőve megkapjuk $\Box$-ot. De persze az input rezolúció egy speciális esete a lineárisnak. Gondolom ezért jutott eszembe.
A jó a lineáris rezolúcióban, hogy teljes, vagyis ha az input kielégíthetetlen, akkor ki lehet hozni lineáris rezolúcióval az üres klózt.
Azért nem ezt választottam implementálni, mert úgy voltam vele, hogy akkor az egész listát is tárolni kéne valahol a képernyőn, és egyre több és több fegyverrel kéne tudnunk lőni emiatt, és tartottam tőle, hogy nem fog elférni már kicsi inputokra sem. Ezért az input rezolúciót választottam és nem tartottam nyilván a listát.
Az SLD rezolúció olyan lineáris rezolúció, amiben a bázisklóz negatív (csupa negatív literált tartalmaz). A tétel azt mondja, hogy
Hogy lehessen veszíteni a játékban, beletettem lépésszám-korlátot. Fogalmam se volt, hogy hány inputrezolúciós lépésben jöhet ki az üres klóz, de belenézve a fentebb linkelt papírba azt láttam (Thm 3.2/1), hogy $2n+1$ biztos elég, ezért beállítottam a $2n$-t lépésszámnak.
Amit benéztem, az az, hogy a $2n+1$ lépésben az $n$ klóz felvétele is benne van, ami miatt $n+1$ lépés is elég kell legyen...
...sőt, arra jöttem rá ma (illetve mivel éjfél elmúlt, tegnap), hogy ha a mátrixban csináljuk az input rezolúciót úgy, hogy fentről lefelé rezolváljuk a második, harmadik,... végül az $n+1$. sorokkal (tehát az inputtal ebben a sorrendben) az első sort (a mobot), mégpedig úgy, hogy az adott sorral akkor rezolválunk, ha az átlóba eső $1$-es változója ütközik a mobban egy $-1$-gyel, egyébként nem. Akkor így $n$ lövésből megvan az üres klóz, minden fegyverrel max egyszer lövünk.
próbáljátok ki: mindig azzal a még nem használt fegyverrel lőjetek a mobra, amiben van olyan ütköző szín, ami a többi még nem használt fegyverben nincs, mindig lesz ilyen, mindegyik fegyverrel max egyszer lőttök és a végére elfogy a mob... kár.
..tehát, a játék túl könnyű, ha csak inputrezolúcióra szorítkozunk, egyszerűen azért, mert túl könnyen leírható, túl szabályos CNF-eket lehet csak legyőzni vele, amikre van egy faék bonyolultságú algoritmus (ha az input CNF-be nem dobálunk felesleges klózokat elterelés címen. mondjuk ezt még lehetne csinálni.)
A következő task tehát átírni a szabályokat, hogy ne input rezolúciót csináljunk.
hanem mondjuk általános lineárisat. ezzel több gond is lesz, pl hogy kielégíthetetlen CNF-et kell generálni valamilyen módon, minimálisat, és a listát is bele kell mesélni a játékba.. :)
- a legkisebb objektumok a játékban színes körök, vagy üresek, vagy telik;
- a pálya közepén lévő mob ilyeneknek egy (bekarikázott) halmaza;
- a pálya alján lévő fegyvereink szintén ilyeneknek egy-egy (bekarikázott) halmaza;
- egy lépésben valamelyik fegyverünkkel rálövünk a mobra;
- alapból ha odaér a lövedékünk, akkor azt a mob lenyeli és az összes színes bigyula halmaza fogja alkotni az új mobot, aki meg is növekszik ettől, de
- halmazról van szó, ha a mobban is és a lövedékben is volt pl piros teli karika, akkor az új mobban is csak egy piros teli karika marad;
- ha két azonos színű teli és üres karika lenne az új mobban, azok kiütik egymást;
- viszont ha több, mint egy ilyen pár van, akkor azonnal elvesztjük a játékot.
- a játék célja pedig, hogy teljesen kiürítsük a mobot, még mielőtt túlnövi a játékteret.
Ha valaki már megcsinálta a logika kurzust, akkor felismerheti, hogy ez nagyon hasonlít a rezolúció nevű módszerre, amivel input konjunktív normálformákról (CNF) tudjuk megmutatni, hogy kielégíthetetlenek. Aki hiányzott: vannak 0/1 értékű logikai változók, ezek a pozitív, negáltjaik a negatív literálok, literálokat vagyolva kapunk klózokat, amiket éselve pedig a CNF-et. Például
$(p\vee\neg q)\ \wedge\ (\neg p\vee\neg q)\ \wedge\ q$
egy CNF, a változók $p$ és $q$, a literálok $p,\neg p,q,\neg q$ és a három klóz: $(p\vee\neg q)$, $(\neg p\vee\neg q)$ és $q$, a harmadik egy egyelemű, avagy unit clause.Mivel a vagyolás és az éselés is kommutatív, asszociatív és idempotens művelet, a sorrend nem számít, és egy klózon belül hogy egy előforduló literál hányszor szerepel, az se számít. Emiatt reprezentálhatunk egy klózt mint literálok egy halmazát, egy CNF-et meg mint klózok halmazát. A fenti pl
$\{p,\neg q\},\{\neg p,\neg q\},\{q\}$
alakba kerül.A rezolúciós algoritmusban egy ilyen alakú CNF az input és listát írunk klózokról. Egy klózt kétféle okból vehetünk fel:
- ha szerepel az input klózok közt, vagy
- ha előáll két korábban felírt klóz rezolvenseként.
Például $\{p,\neg q\}$ és $\{\neg p,\neg q\}$ a $p$-n ütközik, rezolvensük $\{\neg q\}$, aminek $\{q\}$-val a rezolvense a $\Box$ jelű üres klóz. Tehát a példa CNF-ünkből levezethető az üres klóz; a rezolúció helyességi és teljességi tétele azt mondja ki, hogy ez pont akkor történik, ha az input CNF kielégíthetetlen.
So far so good.
A játékban persze a színek megfelelnek egy-egy változónak, a teli karika mondjuk a pozitív literál, az üres karika a negatív literál. Ha a mobba belelövünk és lesz ütköző változó, az kiüti egymást, ez pont egy rezolvensképzés. Ha nincs, akkor simán beleolvad - hát ez ugyan nem volt a rezolúciós szabálykönyvben, de math says ha bevennénk ezt is valid szabálynak, akkor az így kapott rezolúciós variáns is helyes és teljes, szóval miért ne. Ha levezettük az üres klózt, azaz ha kiürül a mob, akkor bizonyítjuk, hogy az input kielégíthetetlen, ez OK.
Volt még az a furán hangzó kitétel, hogy egyszerre két ütköző szín game overt ad; ezt azért kellett bevenni, mert ez annak felelne meg, mintha két változó mentén "egyszerre" rezolválnánk, amit viszont a rezolúciós algoritmus nem enged és okkal nem enged: ha tehetnénk ilyet, akkor olyan esetekben is kijönne az üres klóz, mikor a formula kielégíthető. Pl. a $\{p,q\},\{\neg p,\neg q\}$ input kielégíthető, pl. $p=1,q=0$, de ha szabad lenne két változó mentén egyszerre rezolválni, akkor kijönne belőlük az $\Box$.
Viszont nem szabad, hanem kijönne belőlük rezolvensként vagy a $\{q,\neg q\}$, vagy a $\{p,\neg p\}$. Az ilyeneket (amikben van egy változó is és a negáltja is) triviális klóznak hívják és math says ilyet soha nem érdemes levezetni, ha $\Box$ kijöhet, akkor ilyen nélkül is kijön, legalább ugyanolyan gyorsan. Na ezért tehettem meg, hogy inkább letiltottam azt, hogy egyáltalán próbálkozzanak a userek ilyen esetekben a rezolválással.
Ez a játék viszont egy speciális esete a rezolúciós algoritmusnak, mert
minden lépésben a legutolsóként kapott klózt rezolváljuk egy input klózzal
Úgy egyáltalán, mivel az üres klózhoz az kell, hogy két ellentétes polaritású egységklózt rezolváljunk, eleve csak akkor jöhet ki inputrezolúcióval az üres klóz, ha van az inputban egységklóz is.
Hogy könnyebb legyen a vizualizáció, azt találtam ki, hogy legyen egy inputrezolúciós játék, akkor mindig csak egyetlen klózt kell nyilvántartani a listából (hiszen a lista már elhagyott elemeit nem használjuk fel újra, eldobhatjuk őket), az lesz a mob mindig, és fegyvereink az eredeti input klózok. (Itt nem gondoltam bele pl abba, hogy az eredeti mob is része az inputnak, tehát a mobot ellenségként is és fegyverként is fel kéne venni, hogy teljes legyen a párhuzam az input rezolúció és a játék közt, de ez elmaradt. benéztem, na.)
Már "csak" arra volt szükségem, hogy írjak egy generátort, ami megoldható pályákat (azaz: olyan kielégíthetetlen CNF-eket, melyekre van inputrezolúciós cáfolat) készít. Persze mivel nem tudtam, hogy pontosan miket lehet legyőzni inputrezolúcióval, ezért
ugyanazokból a CNF-ekből lehet inputrezolúcióval kihozni az üres klózt,
mint amikből unit rezolúcióval is ki lehet.
Úgy általában is igaz, hogy egységrezolúcióra a következő algoritmus működik:
- keresünk egy egységklózt;
- azzal megrezolválunk mindent, amit csak lehet;
- elfelejtjük az egységklózt, meg mindent, amiben csak szerepel ez a változó;
- ezt ismételjük, míg meg nem kapjuk az üres klózt vagy el nem fogynak az egységklózok.
Ha felveszek egy $n\times k$-s $A$ mátrixot, aminek egy sora egy klóz, egy oszlopa egy változó, és $A_{i,j}$ akkor $0$, ha a $j$. változó nem szerepel az $i$. klózban, $1$, ha pozitívan és $-1$, ha negatívan, akkor pl a fenti inputunk mátrixa így néz ki:
$\left(\begin{array}{rr}-1&-1\\1&-1\\0&1\end{array}\right)$, első sor $\{\neg p,\neg q\}$, második $\{p,\neg q\}$, harmadik $\{q\}$. Nyilván sorokat meg oszlopokat csereberélhetek, mert se a klózok sorrendje nem számít, se az, hogy melyik változót hanyadiknak veszem fel. Sőt, egy oszlopban átválthatom az előjeleket is (ha minden $p$-ből $\neg p$-t csinálok és viszont, akkor ugyanazok lesznek a valid rezolválós lépések és minden ugyanúgy marad, az üres klózban meg nincs $p$, az nem változik). Ezért feltehetem, hogy az egységklóz, akivel először irtom a világot, az utolsó sorban van, jobb oldalán van az $1$-es, a többi mező $0$.
Ha ezzel a klózzal rezolválok végig mindent, akkor a fölötte levő $-1$ elemeket $0$-ra állítom. Egyébként math says ha van $C_1\subsetneq C_2$, tehát egy olyan $C_1$ klóz, aminél egy $C_2$ bővebb klóz is van, akkor $C_2$-t el is dobhatom, mert $C_1$-et használni mindig jobb, mint $C_2$-t. Ezért ha van egy $\{p\}$ egységklózom, akkor feltehetem, hogy nincs $\{p,q\}$, $\{p,\neg q,r\}$ etc klózom, vagyis az egységklóz $1$-ese oszlopában nincs több $1$-es.
Ha tehát az egységklózzal végigrezolválok minden mást, akkor rajta kívül kinullázom az oszlopát. Megint átrendezve a sorokat és az oszlopokat meg az oszlopon belül az előjeleket feltehetem, hogy a második ágyúzós egységklóz az utolsó előtti sorban alakul ki, az $1$-es az utolsó előtti cella. Balra tőle nem nullázott az előző egységklóz, tehát ott eleve $0$-k voltak. Jobbra vagy volt $-1$, vagy nem, de most már nincs. Ezzel is végignullázzuk a fölötte levő $-1$-eket, $1$-es továbbra sincs az oszlopban (mert azt a klózt eldobtuk volna), alatta nem lehetett nemnulla (mert akkor az utsó sor nem lett volna egységklóz). A következő egységklóz az előző, stb; azt kapjuk, hogy egy egységrezolúcióval cáfolható "minimális" CNF mátrixa pont így nézhet ki:
$\left(\begin{array}{rrrrrr}\star&\star&\star&\star&\ldots&\star\\ 1&\star&\star&\star&\ldots&\star\\0&1&\star&\star&\ldots&\star\\0&0&1&\star&\ldots&\star\\\ldots\\0&0&0&0&\ldots&1\end{array}\right)$,
A fenti tétel szerint tehát ha ilyen mátrixnak sor-oszlop permutálásával és oszlopok mínusz eggyel szorzásával kirakok egy CNF-et, annak lesz inputrezolúciós cáfolata, ami meg nem így néz ki, annak nem lesz (vagy van benne fölösleges klóz/változó, amit nem akartam). Már csak az volt a kérdés, hogy bármelyik elemet kinevezhetem-e mobnak
és hát nem
Ekkor eszembe jutott a lineáris és az SLD rezolúció tétele. Mind a kettő, bizony.
A lineáris rezolúció annyit jelent, hogy kiindulunk egy input klózból (ez lesz a bázisklóz) és minden egyes lépésben a legutóbb kapott klózt rezolváljuk valamivel. Nem feltétlen input klózzal, lehet a listáról is választani! Pl. a $\{p,q\}$, $\{\neg p,q\}$, $\{\neg p,\neg q\}$, $\{p,\neg q\}$ inputból kiindulunk $\{p,q\}$-ból, rálövünk a másodikkal, lesz $\{q\}$, arra a harmadikkal, lesz $\{\neg p\}$, arra a negyedikkel, lesz $\{\neg q\}$, és erre a lista második elemével, $\{q\}$-val lőve megkapjuk $\Box$-ot. De persze az input rezolúció egy speciális esete a lineárisnak. Gondolom ezért jutott eszembe.
A jó a lineáris rezolúcióban, hogy teljes, vagyis ha az input kielégíthetetlen, akkor ki lehet hozni lineáris rezolúcióval az üres klózt.
Azért nem ezt választottam implementálni, mert úgy voltam vele, hogy akkor az egész listát is tárolni kéne valahol a képernyőn, és egyre több és több fegyverrel kéne tudnunk lőni emiatt, és tartottam tőle, hogy nem fog elférni már kicsi inputokra sem. Ezért az input rezolúciót választottam és nem tartottam nyilván a listát.
Az SLD rezolúció olyan lineáris rezolúció, amiben a bázisklóz negatív (csupa negatív literált tartalmaz). A tétel azt mondja, hogy
ha az input Horn formula (minden klózban legfeljebb egy pozitív literál van),
akkor arra az SLD rezolúció teljes.
Ez azért jó most nekünk, meert
- a mátrixunk minden sorában csak egy $1$-es van, az átlón, minden más $0$ vagy $1$, tehát az input Horn formula, az első sora pedig negatív klóz, jó lesz bázisnak;
- math says, hogy Horn-formulán így indítva a lineáris rezolúciót biztos, hogy input rezolúciót fogunk csinálni. (mert a listán végig csupa negatív klóz lesz, azokat meg nem tudjuk egymással rezolválni.)
- beleértve a bázisklózt is, azt se tudjuk még egyszer felhasználni (tehát a mobot nem kell felvenni a fegyverek közé).
Hogy lehessen veszíteni a játékban, beletettem lépésszám-korlátot. Fogalmam se volt, hogy hány inputrezolúciós lépésben jöhet ki az üres klóz, de belenézve a fentebb linkelt papírba azt láttam (Thm 3.2/1), hogy $2n+1$ biztos elég, ezért beállítottam a $2n$-t lépésszámnak.
Amit benéztem, az az, hogy a $2n+1$ lépésben az $n$ klóz felvétele is benne van, ami miatt $n+1$ lépés is elég kell legyen...
...sőt, arra jöttem rá ma (illetve mivel éjfél elmúlt, tegnap), hogy ha a mátrixban csináljuk az input rezolúciót úgy, hogy fentről lefelé rezolváljuk a második, harmadik,... végül az $n+1$. sorokkal (tehát az inputtal ebben a sorrendben) az első sort (a mobot), mégpedig úgy, hogy az adott sorral akkor rezolválunk, ha az átlóba eső $1$-es változója ütközik a mobban egy $-1$-gyel, egyébként nem. Akkor így $n$ lövésből megvan az üres klóz, minden fegyverrel max egyszer lövünk.
próbáljátok ki: mindig azzal a még nem használt fegyverrel lőjetek a mobra, amiben van olyan ütköző szín, ami a többi még nem használt fegyverben nincs, mindig lesz ilyen, mindegyik fegyverrel max egyszer lőttök és a végére elfogy a mob... kár.
..tehát, a játék túl könnyű, ha csak inputrezolúcióra szorítkozunk, egyszerűen azért, mert túl könnyen leírható, túl szabályos CNF-eket lehet csak legyőzni vele, amikre van egy faék bonyolultságú algoritmus (ha az input CNF-be nem dobálunk felesleges klózokat elterelés címen. mondjuk ezt még lehetne csinálni.)
A következő task tehát átírni a szabályokat, hogy ne input rezolúciót csináljunk.
hanem mondjuk általános lineárisat. ezzel több gond is lesz, pl hogy kielégíthetetlen CNF-et kell generálni valamilyen módon, minimálisat, és a listát is bele kell mesélni a játékba.. :)
No comments:
Post a Comment