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..