Saturday, July 5, 2014

Regex illesztés NFA-val, ahogy kell

Tehát a téma még mindig: regexet akarunk illeszteni, gyorsan.


Az előző post végén arra jutottunk, hogy a determinisztikus automata, amit az input regexhez elkészíthetünk, túl nagy is lehet ahhoz, hogy praktikusan használható legyen. (Ha valaki nem hiszi, hogy néha kell hosszú regexekkel dolgozni, nézzen rá az RFC822-re, ami egy regex valid email címre ;-) )

Amit valójában érdemes használni: nemdeterminisztikus automatát.

A nemdeterminizmus, bármilyen számítási modellről (automata, veremautomata, Turing-gép, RAM program stb) is beszélünk, mindig olyasmit jelent, hogy a számítás egy-egy konfigurációjából (egy konfiguráció mindig egy "snapshot" a számítás aktuális helyzetéről, amit ha "kimentenénk" és később visszatöltenénk, akkor onnan folytatni tudjuk a számítást, ahol abbahagytuk. Automata esetében pl. egy konfigurációban az aktuális állapot és az input string még hátralevő része szerepel, ennyi már elég ahhoz, hogy ha leállítjuk a számítást, akkor ennyit megjegyezve később folytatni tudjuk) nem feltétlenül csak egy következő konfigurációba tudunk átmenni, hanem esetleg több rákövetkező is lehet; a számítás során a "gép" választ, hogy ezek közül melyik irányba "akar" továbbmenni. Képzeljük el úgy, mintha a gépnek az lenne a "célja", hogy elfogadja az inputot és tévedhetetlenül "ráérezne", ha csak egyetlen mód is van arra, hogy elfogadja azt, akkor meg is találna egy ilyen utat.

Automaták esetében ez annyit tesz, hogy

  • δ nem függvény, hanem reláció: egy Q×Σ → P(Q) leképezés, azaz egy állapotból és egy betűből a lehetséges következő állapotok egy halmaza van megadva;
  • ez rajzban annyit tesz, hogy lehetnek olyan p állapotok, melyekből nem csak egyfelé lehet menni valamelyik a betűvel, hanem esetleg többfelé is (akár 0-fele is megengedett, ami nyilván azt jelenti, hogy az automata ha ebben az állapotban ezt az input betűt kéne feldolgozza, akkor azonnal el is utasítja az inputot);
  • akkor fogadja el az automata az input stringet, ha lehet úgy haladni a kezdőállapotból egy végállapotba, hogy közben az éleken pont az input stringet olvassuk össze.
Például

egy nemdeterminisztikus automata, ami pl. onnan látszik, hogy q0-ból az a jel hatására el lehet fáradni q0-ba is, q1-be is. (Más "valódi" ok nincs. Igaz, hogy pl. q5-ből nem lehet elmenni sehova, de az nem nagy baj, ilyenkor egy csapdaállapotot, ami nem végállapot, felveszünk, abba átirányítunk minden definiálatlan esetet, őt magát is, és kész is van).
Az látszik, hogy ha q1-be jut a fenti automata, akkor onnan ha négybetűs szót kap, akkor azt q5-ben elfogadja, mást pedig nem. q1-be pedig úgy kerül, hogy először q0-ban olvasgatja az input első karaktereit, aztán "egyszer csak" egy a hatására q1-be ugrik onnan - hogy melyik ez az a, azt vezényli a nemdeterminisztikus kontroll. Látszik, hogy ha az inputban hátulról az ötödik karakter a, akkor az automata ezt az inputot el tudja fogadni - tehát ilyenkor el is fogadja, mert nemdeterminisztikusan "ráérez", hogy épp mikor kellene ugorjon, hogy az a végén jó legyen neki (aka elfogadó állapotba jusson), más esetben viszont nincs olyan futás, aminek a végén elfogad. Tehát, ez a nemdeterminisztikus automata (NFA) pont azokat a szavakat fogadja el, melyeknek hátulról ötödik betűje a.
Persze ezt lehet általánosítani hátulról az n. betűre is, azt n+1 állapotú NFA-val el tudjuk fogadni. A felvezető postban pedig láttuk, hogy ha ragaszkodnánk a determinisztikus változathoz, ahhoz kb 2n állapot kéne
(tudjátok, gombóc)
ezért részesítjük előnyben az NFA-t a DFA-val szemben, mert lényegesen kompaktabb tud lenni.

Ígértem "ezen lehet dolgozni" típusú bekezdéseket is. Nos, az ismert, hogy ha van egy input n hosszú regexem, akkor lehet készíteni vele ekvivalens NFA-t, melynek O(n(logn)2) átmenete van (nemdeterminisztikus automaták "méretére" az állapotszám nem annyira jó jellemző, hiszen az élsűrűség nem adott, mint determinisztikus esetben. Az automata letárolására amennyi tárat kell használjunk, az is az élszámmal tűnik jól mérhetőnek). Van is rá írva algoritmus, ld pl itt vagy egy gyorsabbért itt. A Thompson-algoritmusból származó NFA (mindjárt látni fogjuk) pedig O(n2) méretű.
Ami engem itt érdekel, az az, hogy
a gyakorlatban használt regexek esetében melyik módszer "jobb" a kettő közül?
Mert hiába néz ki kisebbnek az O(n(logn)2), ha esetleg csak csillagászati méretű regexekre győzi le a négyzetest, akkor a négyzetest használjuk. A feladat tehát implementálni és elméleti úton és/vagy generált regexek seregén tesztelve összemérni a két (esetleg három) algoritmust.
Hozzá kell tegyem, hogy ebbe a feladatba páran már belebuktak - úgy tűnik, hogy nem mindenkinek fekszik egy "itt ez a cikk, benne egy algoritmus, kódold le" feladat programtervező informatikusként. Oh well.

Vissza a Thompson-algoritmusra, az először egy lineáris méretű NFA-t épít az input regexhez, melyben vannak üres (spontán, ε) átmenetek is. Ezeket úgy használjuk, hogy ha a (nemdeterminisztikus) automatának van lehetősége valahonnan üres átmenettel (amit most úgy fogok rajzolni, hogy nem írok fölé betűt, máskor esetleg írok fölé ε betűt) átlépni egy másikba, akkor átugorhat és közben az inputból nem kell új betűt olvasson.
Az algoritmus még annyit tud, hogy tetszőleges input regexből olyan NFA-t készít, melynek pontosan egy végállapota van, s ez nem ugyanaz, mint a kezdőállapot, továbbá a végállapotból nem lehet továbbmenni, a kezdőállapotba pedig nem lehet visszajutni. Ha csak egy betűnk van, tehát a regex R = a, arra könnyű ilyen automatát adni:
Ha a regexünk R = R1R2, akkor a rekurzív algoritmus csak "összeragasztja" az R1-hez és az R2-höz készített automatákat: az R1 végállapotát és az R2 kezdőállapotát mergeli.
Ha a regexünk R = R1 + R2, akkor pedig mergeljük a két kezdőállapotot is és a két végállapotot is.
Az iteráció, R = R1*, az egyetlen kicsit komplikáltabb történet: vissza kell tudnunk ugrani a végállapotból a kezdőállapotba, hogy iterációt csináljunk, de emellé még egy-egy új kezdő- és végállapotot kell felvegyünk, hogy ne sérüljön a "kezdőbe nem uthatunk máshonnan, végállapotból nem mehetünk el" feltétel. És kell egy közvetlen ugrás a kezdőállapotból a végállapotba is, hogy a nulla darab ismétlést is megengedjük.

Nem akarok túlzottan belemenni most (és rajzolni se), akit az algoritmus technikai részletei érdekelnek, nézze meg wikin a képeket. (Az uniót ők másképp csinálják.) Elég azt tudnunk most, hogy van olyan algoritmus, ami egy n hosszú regexből egy O(n) állapotú NFA-t épít, melyben vannak üres átmenetek is.

Persze az üres átmenetes NFA nem sokat érne, ha nem tudnánk hatékonyan szimulálni. Meg lehet oldani backtrackinggel, kipróbálva az összes lehetséges számítási útvonalat, hogy van-e közte elfogadó, de ez azért megint egy félelmetesen alulkulturált módszer, ami exponenciális futásidőt eredményez, és ráadásul nem is a rövid regex, hanem a hosszú input string hosszában exponenciálist. Ez kábé a legrosszabb, ami történhet, ha ez lenne a főműsor, akkor nem használnánk NFA-t regex illesztésre.

Van jobb módszer: minden karakter feldolgozása után nyilvántartjuk, hogy melyik állapotokban lehetünk ekkor. Alapból, mikor még nem olvastunk be semmit, lehetünk a kezdőállapotban, vaaagy az abból üres átmenetekkel elérhető bármelyik állapotban (átmehetünk bárhova üres átmenetekkel, ahova csak lehet, még mielőtt egyetlen betűt is beolvastunk). Az összes ilyen állapot halmazával inicializáljuk az aktuális S halmazunkat. Eztán egyesével feldolgozzuk a betűket: ha épp az S halmazban vagyunk valahol, és jön egy a betű, akkor az új halmazunk legyen az összes olyan állapot halmaza, ahova valamelyik S-beli állapotból átléphetünk egy a betű hatására, majd esetleg még néhány üres átmenettel. Ezt a ciklust iteráljuk addig, míg el nem fogy az input.
Formálisabban δ(S,a) nem más, mint az s∈S δ(s,a) halmazból (ide lehet a-val átlépni S-ből) az üres átmenetekkel elérhető összes állapot halmaza (aka lezártja). (Ez nem véletlenül ugyanaz a képzési szabály, mint a determinizáló algoritmusé, aki azt ismeri: a szimulálás során nyilván nem teszünk mást, mint on-the-fly építjük az NFA-val ekvivalens DFA-t és azt szimuláljuk. De nem tároljuk le a DFA-t, így nem kell exp sok hely.)

Ennek az algoritmusnak a futásideje, ha m állapotú a szimulált NFA és n hosszú az input string, O(nm), lépésenként az unió képzése az legfeljebb az m állapotszám darab halmaznak az uniója, innen jön a karakterenkénti O(m) lépés, ami még mindig viselhető, ahhoz képest, hogy a backtrack időigénye O(2n) lenne. Egy, a backtracking hiányosságait kihasználó "gonosz" regexet már egy harminc-negyven karakteres stringre (egy sorra) sem biztos, hogy egy órán belül sikerül illeszteni egy backtracking algoritmussal. Erre a célra az NFA motor egyszerűen nagyságrendekkel jobb, mint pl a backtrack.

Persze ennek ellenére vannak olyan programozási nyelvek, ahol backtrackkel van implementálva a regex illesztés NFA szimulálás helyett. Ahol a nyelv szabvány könyvtárában lévő szabvány implementáció egy backtrack.

Hallani vélem lelki füleimmel az "ó, azok a balfékek" felsóhajtást?
igen?

nos, akkor épp most balfékeztétek le a Java, a PHP, a Perl, a Ruby és számos más mainstream nyelv fejlesztőit. Ezekben bizony backtrack van beégetve.

hogy miért? az egész úgy kezdődött, hogy...
folytköv

Friday, July 4, 2014

Determinisztikus automaták

Egy régi postban már láttunk regexeket, amikkel "pontosan a reguláris nyelvek jelölhetők". Egy input stringre vagy illeszkedik egy regex, vagy nem; ha vesszük az összes stringet, amire illeszkedik az R regex, ezt mondjuk jelölhetjük L(R)-rel (a |R| jelölés is futhat még), és az R regex által megadott nyelvnek hívjuk (mert stringek akármilyen halmazát nyelvnek mondjuk). A regex többek közt azért jó, mert végtelen nyelveket is lehet véges regexekkel jelölni, tehát eggyel kulturáltabb dolog, mint mondjuk a nyelv elemeinek felsorolása egyesével egy kőtáblán. 

Egy másik eszköz, amivel szintén lehet nyelveket megadni, a véges automata. Ebből a "véges" szó annyira be van drótozva, hogy nem is mondjuk ki mostanzól. Egy automatának vannak
  • állapotai, véges sok, legalább egy van - az állapothalmaz jele általában Q
  • bemenő ábécéje, jele általában Σ, olyan szavakat fogad el vagy utasít el, melyek Σ betűiből állnak
  • kezdőállapota, jele általában q0, Q-beli (nyilván. állapot.)
  • végállapotHALMAZa, jele általában ⊆ Q
  • átmenetFÜGGVÉNYe, δ: Q×Σ → Q. Azaz egy állapot és egy betű ismeretében egy állapot az eredmény.

Ha ezeket egyetlen rendszerként kezeljük, akkor rendszerint M = (Q,Σ,δ,q0,F) szokott lenni a sorrend (egyébként: a zárójelekből többféle van. Ez a kerek zárójel, ha ebbe felsorolunk dolgokat, az listát eredményez, tehát a sorrend és a multiplicitás is számít. A kapcsos halmazt deklarál, ott a sorrend nem számít és a multiplicitás sem. Mivel itt számít, hogy az első koordináta az állapothalmaz, a második az input jelek halmaza stb. ezért kerek zárójelet használunk. Az egyenlőség pedig egy értékadó egyenlőség: ezt az öt dolgot így együtt jelöljük M-mel.)

Egy automatát gráfként le is lehet rajzolni: az állapotok lesznek a csúcsok, és az átmenetek a címkézett élek: ha δ(q,a)=p, akkor ebből egy q-ból p-be menő, a-val címkézett nyíl lesz. A kezdőállapotot valamiféle bemenőnyíllal szokás jelölni, a végállapotokat pedig vagy kimenőnyíllal, vagy duplán karikázva.

Például:

Ez egy automata, állapotai Q={q0, q1, q2, q3}, q0 a kezdőállapot, q2 az egyetlen végállapot, a bemenő ábécé {a,b}, az átmenetfüggvény pedig (figyel) például q1-ből a hatására q0-ba viszi az automatát.
Vagyis, a δ függvényt úgy érdemes fejben interpretálni, mint "ha p állapotban vagyok és az a jelet kapom, akkor menjek át q állapotba", ezt fejezzük ki δ(p,a)=q-val.
Ezt értelemszerűen ki lehet terjeszteni szavakra is: "ha p állapotban vagyok és a w stringet kapom, akkor betűnként végigolvasva és minden betű olvasásakor a δ szerint megfelelő állapotba átlépve eljutok a q-ba", ezt fejezzük ki δ(p,w)=q-val. Ha a δ egyértelmű, hogy melyik átmenetfüggvény, akkor szokás elhagyni is az egészet és simán pw=q-t írni.
A fenti automata pl. ha q1-ben megkapja az aabaa stringet, akkor a q0,q1,q3,q2,q3 állapotok végiglátogatása után q3-ba jut, tehát q1aabaa=q3.
Az automata akkor fogadja el az input szót, ha az q0-ból egy végállapotba viszi, és elutasítja, ha nem végállapotba. (formálisan elfogadja w-t, ha q0w ∈ F.) Az összes M által elfogadott szó nyelve pedig L(M).
A fenti automata például akkor fogad el egy szót, ha az páros sok a-t tartalmaz és van benne legalább egy b betű. Ezt onnan láthatjuk most, hogy a bal felső állapotból a szó hatására a bal alsóba kell jussunk. Az a betű mindenképp a bal-jobb térfelet váltja, tehát ha páros sok jön belőle, akkor a bal oldalon, ha páratlan sok, akkor a jobb oldalon végzünk. Lefelé pedig csak a b betűvel lépünk, tehát abból is kell egy. Ezek után teljesen mindegy, ha jön további b betű, az már nem váltja az állapotot.
Erre van regex is, pl.
(aa)*b(ab*ab*)*+a(aa)*b(ab*ab*)*ab*

hát nem túl szép, nem túl rövid, nem túl elegáns, de jobbat nem tudok. (aki igen: feel free to comment :-) ) A regex első fele kezeli azt az esetet, mikor az első b előtt is és utána is páros sok a betű jön, a második fele meg azt, mikor páratlan-páratlan sok. (Hozzáteszem, hogy most klasszikus, elméleti regexről beszélek, ezért nem használok pl. lookaheadet. Majd fogok.)

Nem véletlen, hogy ehhez az M automatához van ekvivalens (ugyanazt a nyelvet jelölő, mint amit az automata elfogad, avagy L(M)=L(R)) R regex, mert
pontosan a reguláris nyelvek ismerhetők fel automatával.

Sőt, van olyan algoritmus is, ami az input regexből készít egy ekvivalens automatát. Ez azért jó, mert a regexes postban nem beszéltem arról, hogy hogy is lehet regexet illeszteni, vagyis eldönteni, hogy az input R regex illeszkedik-e az input szövegre vagy sem - nos, ezt például automatával már könnyű, hiszen csak végig kell olvasnunk. Tehát illesszünk regexet úgy, hogy először készítünk egy vele ekvivalens véges automatát, majd annak beadjuk a stringet. (Az automata O(m) lépésben végigolvassa az m hosszú input stringet, tehát gyors is az illesztés.)
OK?
NEM
mert a regex - DFA konverzió (btw a DFA a Deterministic Finite Automaton rövidítése) exponenciális méretű automatát is eredményezHET legrosszabb esetben! Például az Σ*aΣΣΣ..Σ regex, ahol az a után n darab Σ áll, ami annyit mond, hogy hátulról az n+1. betű a kell legyen (erről nem állítom, hogy gyakorlati oldalról feltétlen motivált lenne, viszont kegyetlenül el tud bánni az algoritmusunkkal), az ezzel ekvivalens legkisebb automata is 2n állapotú, ami
gombócból is sok.
(déja vu.)
Ezért valójában nemdeterminisztikus automatákat szokás használni, üres átmenettel, mert arra
van lineáris konverzió
és sokat nem ront az illesztési sebességen. Lesz róluk post.
folytköv

Thursday, July 3, 2014

Grafilogika és társai - unique megoldások, mitől nehéz egy input?

Az megvan, hogy a Grafilogika NP-teljes? :-)

Csakhogy, az újságokban látható rejtvények egyvalamiben nagyon különböznek az eddig tárgyaltakról: pontosan egy megoldásuk van. Ez a grafilogika esetében momentán egy szép kép is.

Ha pedig a célunk az, hogy egy rejtvénytípusban kiváltsuk a (költséges) szakértőt, pályatervező mestert, akármit egy (eladható :P ) programmal, akkor a feladat: feladványok generálása, melyeknek pontosan egy megoldásuk van, és ezeknek a nehézségét is valamilyen módon mérni kell. Az se hátrány, ha gyorsan generálunk. Ugyanakkor biztosítanunk kell, hogy tényleg egyetlen megoldás legyen - ha ezt egy solverrel ellenőrizzük le, akkor a generált feladvány annyira nem lesz nehéz, hiszen egy solver (a mienk) meg fogja tudni oldani. Vagy, eleve a generálási módszer kell olyan legyen, ami garantálja a unique megoldhatóságot.

Létezik persze olyan SAT-variáns (called UNIQUE-SAT), ami ezt akarja elkapni: az input CNF-re a specifikáció annyi, hogy igen-t kell mondani, ha pontosan egy kielégítő értékelése van, nemet akkor, ha kielégíthetetlen, egyébként pedig bármi elfogadható. (Az ilyen típusú problémákat promise problémának is nevezik: "megígérem, hogy 0 vagy 1 megoldás van, mondd meg, melyik az igazság" -- ha az ígéretet "megszegi" az input, akkor bármit válaszolhatunk.)

Itt a "hagyományos" visszavezetés-fogalom nem alkalmazható: lehet, hogy a visszavezetésünk (mint pl. amit láttunk a SAT-ból 3SAT-ba is) egy olyan példányból, melynek pontosan egy megoldása van, egy olyat készít, melynek több is. (De lehet olyan visszavezetést is készíteni, mely a kielégítő kiértékelések számát is megtartja, az ilyet parsimonious vagy magyarul talán "takarékos" visszavezetésnek hívják).

Mármost a Valiant-Vazirani tétel azt mondja, hogy ha a UNIQUE-SAT-ra van polinomidejű algoritmus, akkor NP = RP. Ez annyit tesz, hogy az összes NP-beli problémára van hatékony randomizált algoritmus, ezt is úgy hisszük, hogy nem igaz. Akárhogy is, jó okunk van azt hinni, hogy

az NP-teljes problémák akkor is nehezek maradnak, ha unique a megoldásuk.

Legalábbis jó részük, ha már egyszer a SAT-ra igaz ez.

A másik lényeges kérdés megint az, hogy még ha a problémára tudjuk is, hogy NP-nehéz, az csak azt jelenti, hogy minden eddig ismert algoritmusra vannak olyan inputok, amik az adott algoritmust bekergetik egy exponenciális lassú futásba. De ez csak annyit mond, hogy "ez az input ennek az algoritmusnak nehéz". Viszont egy-egy jól összeállított rejtvényről lehet az a vélekedés, hogy uniforman nehéz: valamilyen értelemben minden generikus algoritmus számára nehéz. De mit jelent ez? A másik kérdés tehát az, hogy

mitől nehéz egy adott példány 

generikus értelemben, tehát mikor tudjuk (ha tudjuk) azt mondani egyáltalán inputok egy családjára, hogy ezek "nehezek"?

Maradva az elkezdett aknakeresős témánál, egy remek feladat lehet (ami engem is nagyon érdekel) a következő: egy generátor fejlesztése, mely olyan (aknakereső, grafilogika, eternity, akármi) feladványokat állít elő lehetőleg gyorsan, melyekre garantált, hogy pontosan egy megoldásuk van, és egy olyan "metrikát" előállítani, mellyel az előállított példányok "nehézsége" mérhető. Hogy egy ilyen metrika mennyire lehet objektív, az szakirodalmazás kérdése :-) és a választott problémától függ, természetesen. Még jobb lenne, ha a generátor konzisztensen képes lenne nehéz példányokat generálni.
A feladat eléggé beleharap az automatikus tartalomgenerálás területébe, és ebben a köntösben ipari szemszögből elsősorban persze a "random" pályás játékfejlesztés vonalon lehet profitálni belőle.

Wednesday, July 2, 2014

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.

Tuesday, July 1, 2014

SAT solverek

Ahogy az NP-teljességes postban is láttuk, a SAT egy központi probléma, aki azt megoldja ügyesen, az sok minden mást is. Ezért a népek mindenfelé a világban SAT solvereket fejlesztenek (a solver attól solver, hogy nem csak igen/nemet válaszol, hanem ha kielégíthető az input CNF, akkor illik is adjon egy kielégítő kiértékelést).

Persze van minden évben verseny is: a SAT Competition. Itt az induló programoknak többféle módon generált, kielégíthető vagy kielégíthetetlen, "nehéz" CNF-eket adnak (hogy egy példány mitől lesz "nehéz", az persze jó kérdés -- erre nem tudok jó definíciót, mindenesetre olyanokat próbálnak adni, ami az általános solverek többségének tényleg "kihívás"), pontozzák őket stb.

Azt érdemes tudni, hogy ezek a solverek gyakran csak 3SAT-ot tudnak megoldani. A 3SAT attól 3SAT, hogy minden klózban csak három literál szerepelhet, nem több. Ez nem nagy baj, mert a tetszőleges CNF-et ilyen 3CNF-re lehet alakítani úgy, hogy ne változtassuk meg a kielégíthetőséget (igen, ezt hívtuk az előbb visszavezetésnek), a következő módon: általában egy n-literálos (k1 V k2 V ... V kn) alakú klózból készítünk egy
(k1 V k2 V x1) & (-x1 V k3 V x2) & (-x2 V k4 V x3) & ... & (-xn-3 V kn-1 V kn)

alakú CNF-et. Magyarán bevezetünk teljesen új "kapcsoló" változókat, ezek fent az x-ek, és a háromtagú klózokat úgy kötjük velük össze, hogy két szomszédosba kerüljön ugyanaz az xi, egyikbe pozitívan, másikba negatívan. Nyilván így a két szélső klózba az eredeti literálokból kettő-kettő, a belső klózokba egy-egy kerül. Ha ezt minden, háromnál több literált tartalmazó klózra megcsináljuk (mindig teljesen új kapcsoló-változókat bevezetve), a max három hosszúakat pedig békén hagyjuk, akkor az eredmény egyrészt 3CNF lesz, másrészt be lehet látni, hogy ha az eredeti CNF kielégíthető volt, akkor annak egy kielégítő értékelését alapul véve "be tudjuk lőni" az új x-ek értékét úgy, hogy az új formula is kielégíthető legyen. Ha viszont kielégíthetetlen volt, akkor ez a generált 3CNF is kielégíthetetlen lesz.
Ez pontosan az, amit visszavezetésnek hívunk: választartó, gyors inputkonverzió.

Vagyis a SAT visszavezethető a 3SAT-ra. Ha egy NP-nehéz problémát vissza tudunk vezetni valamire, akkor az is NP-nehéz lesz (bármit vissza tudunk vezetni rá NP-ből: először konvertáljuk az inputot az ismerten NP-nehéz probléma inputjává, majd eztán ezt a két probléma közti konverziót hajtjuk végre az eredményen, amit kapunk, az jelen esetben egy 3CNF lesz, bármiből is intultunk). Nyilván NP-ben is van, hiszen ugyanúgy tanúsítvány-rendszert alkotnak a kielégítő kiértékelések, mint a sima SAT-nál.

Tehát a 3SAT is NP-teljes.

Ezért, vissza a solverekhez, a solverek jelentős része eleve úgy van megírva, hogy csak 3CNF-eket támogat. Ezt és a visszavezetést azért jó észben tartani, mert ha SAT solverre van szükségünk (hamarosan lesz), akkor lehet, hogy az akármilyen formulánkból, amit gyártottunk (pl. az aknakeresős példában vszg nem pont egy 3CNF-ünk lett), először nekünk kell kézzel egy s-ekvivalens 3CNF-et gyártani a fenti módon (s-ekvivalens azt jelentette, hogy kielégíthetőből kielégíthetőt, kielégíthetetlenből kielégíthetetlent kell készítsünk. Logikából a skolemizálás pl ilyen volt), és azt beadni a kedvenc SAT solverünknek.

Onnan kezdve, hogy van egy rakat, pl. a SAT Competition weblapról elérhető solver, többségük free és open-source, sok NP-beli problémát megtámadhatunk akár úgy is, hogy írunk egy visszavezetést, ami az aktuális problémánk inputjából készít egy megfelelő CNF-et, és arra egy világbajnos solvert ráengedünk.

Meglepő, de időnként lényegesen jobb eredményt érünk el ezzel, mintha írnánk egy kicsit okosított backtracket. És gyorsabban is megvan az implementáció. Az, hogy backtrackkel mérjük össze a visszavezetés+SATsolver hatékonyságát, az nem kell zavarjon senkit: ne felejtsük el, hogy ezt NP-teljes problémákra csináljuk. Azokra meg exponenciálisnál jobb algoritmust nem ismerünk, tehát a backtracknél lényegesen jobb algoritmusunk nem nagyon lesz..
Máskor persze előfordul, hogy a mezei backtrack csúnyán elveri a visszavezetős-solveres megoldást.
Hogy ez pontosan mikor történik, jó kérdés*.

A versenyről azt is érdemes tudni, hogy mindig van "Industrial" vagy újabban "Application" track, ami tényleg azt jelenti, hogy egy cég egy optimalizálási problémáját, amivel (általában) az adott évben küzdött, konvertál(tat)ta át CNF-re és ezeket próbálják megoldani a solverek. A "Crafted", "handmade" meg "Combinatorial" trackek (mikor épp hogy hívják) ezzel szemben meg kézzel gyártott szintetikus formulák. Ha gyakorlatban akarjuk alkalmazni valamelyik solvert ilyesmire, akkor én az ipari track érmesei közül választanék...

Ahogy megnéztem most a listát, amit abból már láttam korábban:
  • minisat, open-source, gcc, van C# portja is, szépen fordul, jó helyezéseket ér el
  • glucose, a minisatra épül, tehát gcc
  • lingeling és változatai, mint a fentebbiek.
Mostanában ez a három viszi az ipari tracket (vannak mindhez persze hackek, egyesek letöltik valamelyiket, átírnak vagy felcserélnek benne pár sort és beküldik új versenyző néven), ezekkel érdemes próbálkozni, ha egy (esetleg branch-and-bounddal ellátott) backtrackinget nincs kedve / ideje az embernek leimplementálni, kigondolni jó vágási feltételeket és heurisztikákat, ezekben a solverekben van bőven heurisztika, és könnyen lehet, hogy megoldják a problémát. Beletanulni meg csak egyszer kell a solverek futtatásába és paraméterezésébe és máris van egy széles körben használható eszköz a kezünkben -- amit meg kell csinálni minden problémánál, az maga az inputkonverzió.

Amire a következő postban fogunk látni két példát, egy olyan esetet, mikor a visszavezetéses technika katasztrofálisan lassúnak bizonyult, és egy olyat, mikor szépen elvert egy heurisztikus backtrackinget.
folytköv

*jó kérdés == engem érdekel. Ha mást is érdekel, szóljon, könnyen lehet, hogy megegyezünk egy szakdoga- vagy diplomadolgozat témában..

NP-teljesség: az elmélet

Sokszor fogom használni azt a szót, hogy egy probléma NP-nehéz vagy NP-teljes. Azoknak viszont, akik sem bonyelmet, sem számtudot nem tanultak még, lehet, hogy ez nem mond túl sokat; ezt a lyukat próbálom betömni. Először is, hogy intuíciónk legyen:

Egy probléma NP-teljes, ha megoldását ellenőrizni könnyű,
de előállítani nehéz.

Ilyen például a SAT probléma, ami a következő (problémákat input/output specifikációval adok meg) :

  • input: egy konjunktív normálformájú formula (CNF),
  • output: 1, ha kielégíthető a formula (be lehet állítani 0/1-re a változóit úgy, hogy a végeredmény 1 legyen), 0 egyébként (ha mindig 0-t kapunk).
Először is, kiszámítani, hogy egy CNF kielégíthető-e vagy sem, persze ki lehet: egy félelmetesen alulkulturált módszer pl. kipróbálni az összes lehetséges értékadást. Ha van n változónk a formulánkban, ez 2n lehetőség, ami

gombócból is sok.

Ha mondjuk van száz változónk (most lehet, hogy van, aki azt hiszi, hogy ez sok - nem az), az 2100 próbálkozás, ami egy 30-jegyű szám. Százbites. Ha másodpercenként 1010 próbát végzünk (egy 10GHz-es gép minden órajelében egyet, extrém munkavégzés), akkor 4*1012, azaz

négybillió év alatt

végzünk is. Ez most ad egy jó képet arról, hogy mit értünk "előállítani nehéz" alatt. Persze abból, hogy van egy buta algoritmusunk, még nem kell, hogy bármi következzen, lehet, hogy van jobb is. Néhányan már látták biztos a rezolúció nevű csodát, ami pont erre a problémára egy algoritmus, de
a rezolúció is exponenciális időigényű,
ráadásul még exponenciális tárat is eszik hozzá legrosszabb esetben, szóval annyira nem nagy megtakarítás.

A fentiből még talán magyarázatra szorul az "exponenciális" szó, ez nyilván valami cn vagy hasonló alakú függvény, valamilyen c-re és n-re. (Valójában nem csak n-t, hanem tetszőleges polinomot megengedünk kitevőben, de ez most nem olyan lényeges.) A futás- és tárigényről szóló képletekben n mindig az input mérete lesz, pl a SAT esetében az egész formulának mint pl stringnek a hossza. Nyilván még ha karakterenként új változó is jön mindig, akkor is egy n hosszú formulában legfeljebb n változó szerepel, így jön ki a 2n-es futásidő (precízebben, O(2n)-es futásidő -- az O(f(n)) azt jelenti megközelítőleg, hogy legfeljebb f(n), legalábbis valamilyen n-től kezdve.)

A helyzet az, hogy a SAT problémára a mai napig nem tudott senki olyan algoritmust mondani, mely szubexponenciális idő alatt garantáltan megoldja: a legjobb algoritmus ha jól emlékszem, 1.3n időigényű, ami kb 300 változóra hozza ugyanazt az időlimitet, mint a 2n-es 100 változóra, szóval not that much of a gain.
De senki nem tudta bebizonyítani, hogy nincs polinom időigényű (n, n2, n3, ilyesmi) algoritmus - ez a számítástudomány legismertebb és legnagyobb nyitott kérdése, a

P =?= NP

-ként is ismert, melyet meg lehet úgy is fogalmazni, hogy vajon

megoldható-e a SAT polinomidőben vagy sem?

Jó, mondjuk egy n100 időigényű algoritmus némi jóindulattal is a "mérsékelten hasznos" kategóriában indul, ott is a vigaszágon, de a gyakorlati tapasztalat azt mutatja, hogy ha valami gyakorlati problémára van polinomidejű algoritmus, akkor arra előbb-utóbb lesz kellemesen alacsony kitevőjű polinomiális algoritmus is.

Még nem szóltam az "ellenőrizni könnyű" részről. Úgy képzeljük, hogy ha egy kérdésre egy válasz "igen", akkor arra van valamiféle bizonyíték is. Például ebben az esetben ha egy CNF a SAT-nak egy "igen" példánya, azaz kielégíthető, az azért van, mert van egy kielégítő kiértékelés, a változók egy értékadása, ami igazra értékeli a formulát.
Egy ilyen kielégítő értékadás egy "tanú" az inputra.

Egy eldöntési (ez annyit jelent, hogy a kérdésre a válasz igen vagy nem) probléma akkor van NP-ben, ha van hozzá olyan tanúsítvány-rendszer, ami a következőket tudja:

  • Egy I input ha "igen" példány, akkor van azt igazoló tanú.
  • Egy I input ha "nem" példány, akkor nincs ilyen tanú.
  • A tanúk "rövidek": van olyan p polinom (n, n2, stb), hogy az n hosszú inputhoz tartozó tanúk legfeljebb p(n) hosszúak.
  • A tanúk "könnyen ellenőrizhetőek": ha adott egy I input és egy T tanúsítvány, akkor azt szintén polinomidőben le tudjuk ellenőrizni, hogy T tényleg tanú-e I-hez.
Az utolsó két feltételt így együtt egyébként hívják "polinomidőben verifikálhatóság"-nak is.

A SAT-ra visszatérve: itt az input CNF-ekhez a változók kielégítő kiértékelései a tanúsítványok. Nyilván kielégítő kiértékelése pontosan a kielégíthető formuláknak van (ezért az első két feltétel azonnal teljesül is), a változó-értékadás n-bites, azaz rövid (megint miért - mert nem lehet több változó, mint amilyen hosszú az egész formula), és ha van egy értékadás, azt lineáris időben ki is lehet értékelni (csak végig kell menni a formulán és minden egyes klózra megnézni, hogy van-e benne 1 értékű literál - ez tényleg megy lineáris időben, ha az elején a kiértékelést egy tömbbe rakjuk). Ezért mondhatjuk, hogy a SAT NP-ben van, avagy polinomidőben verifikálható.

Az NP betűszó egyébként a nemdeterminisztikus polinomidő-ből jön, megközelíthetnénk az NP osztályt úgy is, mint a nemdeterminisztikus polinomidejű algoritmussal eldönthető problémák osztályát, de most a nemdeterminizmusra nem térnék ki.

Néhány további NP-beli probléma és a hozzájuk kapcsolódó tanúsítvány-rendszer, ami miatt NP-beliek:
  • Elérhetőség: input egy n-csúcsú gráf, el lehet-e jutni az első csúcsából az n. csúcsába? Egy tanúsítvány-rendszer: a G gráf 1-es csúcsából az n-es csúcsába vezető út. (Nyilván az út csak n hosszú lehet maximum, könnyű ellenőrizni, hogy tényleg út-e, hisz csak az éleket kell ellenőrizni, hogy tényleg élek-e, és pont akkor van út 1-ből n-be, ha el lehet jutni, hát ez az elérhetőség definíciója.)
  • Összetett számok: input egy N szám (binárisan! akkor ez logN bites input), kérdés: összetett szám-e? Egy tanúsítvány: az N szám egy valódi osztója egy tanú (rövid, az oszthatóságot könnyű tesztelni, és pont az összetett számoknak van valódi osztójuk, attól összetettek).
  • Hamilton-út: input egy G gráf, van-e minden csúcsán pontosan egyszer átmenő út. Tanú: maga a Hamilton-út.
  • Aknakereső: input egy részlegesen kitöltött Aknakereső-tábla, kérdés: konzisztens-e, azaz le lehet-e rakni úgy az aknákat, hogy minden felfedett szám mellé pont annyi akna kerüljön, amennyit a szám mond. Tanú: egy jó lerakás.
...stb. Rengeteg optimalizálási probléma is megfogalmazható "van-e olyan megoldás, aminek a költsége legfeljebb X" formában, ily módon ezek is NP-be esnek, ezért az NP egy gyakorlatból nagyon motivált osztály. (Várhatóan lesz sok NP-s poszt még, ha valakit ez még nem győzött meg :) )


Az "NP-teljes" annyit jelent intuitíve, hogy ugyan NP-beli a probléma, de azok közül a(z egyik)

legnehezebb.

A fenti listában pl. a Hamilton-út, az Aknakereső és a SAT NP-teljesek.
Az elérhetőségre és a prímtesztelésre ezzel szemben van polinomidejű algoritmus.
Az NP-teljes problémák egyikére se talált még senki, és nem is tudta bebizonyítani, hogy ilyen nincs.
(Próbálkozások azért vannak. Jó nincs köztük.)

Ahhoz, hogy ezt a teljességfogalmat kicsit mélyebben megértsük, meg kell ismerjük a 

visszavezetés

fogalmát, amit arra használunk, hogy tudjuk mondani, hogy az Y probléma legalább olyan nehéz, mint az X probléma (azért nem "nehezebb"-et mondok, mert egyforma nehezek is lehetnek). Ez a következőképp szól:
az X-nek Y-ra való visszavezetése egy gyors inputkonverzió, mely tartja a választ. Azaz, egy olyan f függvény, mely X inputjait alakítja át Y inputjaira oly módon, hogy ha az eredeti I input az X-nek "igen" példánya, akkor az átalakított f(I) input az Y-nak lesz "igen" példánya, "nem" példányból pedig "nem" példány lesz. Ez a választartás. A "gyors" pedig annyit tesz, hogy polinomidejű (ez már talán nem lepett meg senkit: az ökölszabály az, hogy valami akkor elég gyors, ha polinomidejű).

Például, az Aknakereső visszavezethető a SAT-ra: minden (i,j) mezőhöz hozzárendelünk egy x(i,j) logikai változót, amit akkor szánunk 1-re állítani, ha azon van akna és 0-ra, ha nincs, ezután csak össze kell éselnünk a számok által mondott feltételeket (pl egy 5-ös érték (i,j)-n azt mondja, hogy a körülötte levő 8 mezőből pontosan 5-ön van akna, amit ki lehet fejezni logikai formulával, hogy 8 változó közül pontosan 5 igaz. Akkor van hozzájuk CNF is. Ezeket kell összeéselni.), és ha a kapott formula kielégíthető, akkor az pont azt jelenti, hogy le tudunk rakni aknákat a táblára. (Ha ez gyors volt, nem baj, most nem olyan lényeges, látunk még ilyet. A lényeg, hogy van olyan gyors módszer, ami Aknakereső inputból SAT inputot készít választartó módon, ezért az Aknakereső visszavezethető a SAT-ra.)

Azért jelenti ez azt intuitíve, hogy az Aknakereső legfeljebb olyan nehéz, mint a SAT, mert ha a SAT-ra van algoritmusunk, akkor innen kezdve van az Aknakeresőre is: az input aknász táblát először átkonvertáljuk logikai formulává a visszavezetéssel, aztán ráengedjük a SAT solvert és a válaszból a választartás miatt megtudjuk, hogy az eredeti aknász táblánk konzisztens volt-e vagy sem.
(Amúgy vegyük észre, hogy ezzel egy kicsi, tízszer tízes táblából is hirtelen születik egy százváltozós SAT...)

Hogy a SAT NP-teljes, az azt jelenti, hogy NP-ben van és
minden NP-beli probléma visszavezethető rá.

mind. Az összes. Az elérhetőség, a Hamilton-út, az Aknakereső, a prímtesztelés, a TSP, a lineáris optimalizálás, minden NP-beli probléma. Ha a SAT-ot meg tudnánk oldani polinomidőben, akkor minden NP-beli problémát (inputkonverzió+SAT solver futtatásával) meg tudnánk oldani polinomidőben.
És mivel ez még senkinek nem sikerült, ezért a legtöbben úgy véljük, hogy nincs is ilyen algoritmus, vagyis P<>NP.

Ha egy probléma nehéznek látszik, és meg tudjuk mutatni, hogy NP-teljes (az NP-nehéz egyébként annyit jelent, hogy minden NP-beli probléma visszavezethető rá, de nem feltétlenül van NP-ben. Az ilyen problémák még sokkal nehezebbek lehetnek, mint bármelyik a fentiek közül. Egy ilyen pl. a Lemmings. Meg a Sokoban. Meg a sakk, a hex, és általában a jobb kétszemélyes játékok. A reguláris kifejezések ekvivalenciája is. Vannak nagyon nehéz problémák..), tehát ha meg tudjuk mutatni, hogy NP-teljes, az jó érv arra, hogy ne akarjuk feltétlenül megoldani, hanem például
elégedjünk meg közelítő megoldásokkal,
vagy
elégedjünk meg olyan algoritmussal, mely csak bizonyos inputokra működik,
és itt lép be a képbe a mestint, a heurisztikák és az approximáció.

Legközelebb esettanulmányokkal folytatom, lássuk ezt "élesben".