SAT problémák részekre bontással történő megoldása

OData támogatás
Konzulens:
Dr. Mann Zoltán Ádám
Számítástudományi és Információelméleti Tanszék

A logikai formulák kielégíthetőségének problémája (Boolean satisfiabliliy probléma, röviden csak SAT probléma) a számítástudomány egyik legismertebb és legtöbbet vizsgált kérdésköre. Egyaránt kiemelt jelentősége van elméleti és gyakorlati szempontból, mivel egyrészt rengeteg különféle absztrakt probléma vezethető vissza ilyen feladatra, másrészt a gyakorlatban is számtalan különböző mérnöki alkalmazási területen előkerül. Mivel a probléma NP-teljes, sajnos a megoldására mindmáig nem ismerünk polinomiális futásidejű algoritmust.

A SAT problémák megoldása terén ma ismert legjobb, úgynevezett CDCL típusú algoritmusok már nagyon bonyolult és ötletgazdag módszerek, amik bizonyos alkalmazási területeken sokszor hatalmas méretű problémákat is nagyon rövid idő alatt meg tudnak oldani. Ugyanakkor sok területen kerülnek elő még nagyobb méretű, vagy az előzőektől teljesen eltérő jellegű problémapéldányok, amelyekkel még ezek az algoritmusok sem tudnak elfogadható időn belül megbirkózni. Ezért továbbra is kiemelten fontos a SAT-megoldó algoritmusok további gyorsítása, amellyel világszerte rengeteg kutató és szakember foglalkozik.

Egy lehetséges megközelítés a további gyorsításra a probléma részekre bontása; a dolgozat során azt vizsgáltam, hogy ezen az ötleten alapuló módszerek segítségével tudjuk-e esetleg még tovább fejleszteni a modern SAT-megoldók hatékonyságát. Mivel a megoldó algoritmusok futásideje exponenciális jellegű a probléma méretének függvényében, ha az algoritmus futása során elérjük, hogy a formula kisebb, egymástól független részformulákra essen szét, akkor joggal remélhetjük, hogy a két részformula kielégíthetőségének az eldöntése kevesebb ideig tart, mint az eredeti formula megoldása.

A szakdolgozatom során megterveztem és implementáltam egy CDCL típusú SAT-megoldó algoritmust, amely rendelkezik az ilyen algoritmusok legfontosabb tulajdonságaival és technikáival, többek között klóztanulással, nem-kronologikus visszalépéssel, újraindításokkal és a VSIDS heurisztikával. Szintén leprogramoztam a hipergráfok partícionálására szolgáló Fiduccia-Mattheyses heurisztika több különböző változatát, illetve különféle további fejlesztéseket dolgoztam ki olyan hipergráfok esetére, amelyeken ez a heurisztika gyengébb eredményeket ad. Kidolgoztam több stratégiát is arra vonatkozólag, hogy az előbbi módszerekkel megtalált partícionálásokat hogyan lehet a SAT-megoldó futása során az algoritmus minimális módosításával felhasználni úgy, hogy ennek hatására a megoldandó probléma minél hamarabb diszjunkt részproblémákra essen szét, és a megoldó algoritmusnak lehetősége legyen ezeket a részproblémákat egymástól függetlenül megoldani.

Az eredeti algoritmust és a különböző partícionálást használó változatok futásidejét SAT problémák több különböző csoportján hasonlítottam össze, melyek között egyaránt voltak mérnöki alkalmazási területekről származó és véletlenszerűen generált példányok. Az empirikus vizsgálatok azt mutatták, hogy több problémacsoport esetében is akadt olyan részekre bontási módszer, ami hatékonyabbnak adódott az eredeti algoritmusnál. A vizsgálatok során azt tapasztaltam, hogy az úgynevezett duális partícionálást alkalmazó módszer határozottan gyorsabban oldja meg a kisebb számú klózt tartalmazó nehéz problémákat, mint az algoritmus eredeti verziója. Ugyancsak azt találtam bizonyos nagyobb méretű, gyakorlati alkalmazási területekről származó problémák esetén, hogy egy másik, az úgynevezett modellgenerálós módszer nagyságrendekkel hatékonyabbnak adódik a kiindulási algoritmusnál. Az eredmények jól rámutatnak arra, hogy a formulát részekre bontó stratégiák sokszor gyorsabb működést eredményeznek bizonyos tulajdonságú vagy méretű SAT problémákon, így érdemes lehet alkalmazni őket a mai vezető SAT-megoldókban.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.