SAT-solverek gyorsítása best-first search algoritmussal

A mérnöki gyakorlatban a legfontosabb problémák jelentős részére igaz, hogy jelenleg nem ismert minden példányukat gyorsan (polinomidőben) megoldani képes algoritmus. Ezeket összefoglaló néven NP-teljes problémáknak nevezzük. Az első ismert NP-teljes probléma a Boolean Satisfiability (SAT), ahol egy logikai formula változóinak próbálunk úgy értéket találni, hogy a kifejezés igazra értékelődjön ki. Az ipari alkalmazásokban gyakran fordulnak elő olyan problémák, melyeket könnyen megfogalmazhatunk SAT-problémaként. Ezek nehézsége a mai számítógépek számítási kapacitását is keményen próbára teszi. A kutatása éppen emiatt népszerű, olyannyira, hogy évente SAT-versenyt is rendeznek. Itt saját készítésű algoritmusokkal lehet részt venni, és a cél probléma példányok minél gyorsabb megoldása.

A jelenlegi SAT megoldó algoritmusok (solverek) legnagyobb problémája az, hogy bár sok esetben gyorsan oldják meg a problémákat, néha a futási idő a szokásosnál nagyságrendekkel hosszabbra is nyúlhat. Ennek csökkentésére a jelenlegi leghatékonyabb módszer az, hogy a keresést bizonyos időközönként újraindítjuk. Valószínűsíthető, hogy ekkor hamarabb eredményre jutunk, mintha az algoritmust beavatkozás nélkül futtatnánk. Ez a megoldás azonban közel sem tökéletes: a keresés elért részeredményei az újraindításnál elvesznek, valamint semmi sem garantálja, hogy az új futtatásnál valóban gyorsan eredményt kapunk.

A TDK dolgozatomban az újraindítás helyett egy másik módszert alkalmazok a futásidők szórásának csökkentésére. Ez a "legjobbat először'' (best-first search) algoritmus, amely a futása során gyűjtött adatok alapján próbálja kitalálni, merre kell keresnünk a megoldás minél hamarabbi eléréséhez. Ezáltal a solver képes lesz arra, hogy változtasson a keresési stratégiáján, de az addigi részeredményei megtartása mellett.

A jelenlegi SAT solverek nem összeegyeztethetők a hagyományos best-first search kialakításával, ezért az alkalmazáshoz az algoritmus jelentős módosítására volt szükség. Fontos kérdés volt az is, hogy pontosan milyen adatok alapján tudjuk megítélni a megoldás közelségét. A tervezés után a kész algoritmust a MiniSatba, egy gyors, de könnyen bővíthető SAT solverbe implementáltam. Az eredmények kiértékelését és a finomhangolást egy algoritmusok tesztelését segítő szoftvercsomag, a BCAT könnyítette meg.

A tesztelés során kapott eredmények azt mutatják, hogy ezzel a módszerrel számottevően gyorsítottam a különféle problémapéldányok megoldását, és sikerült csökkentenem a futásidők hatalmas különbségét is.

szerző

• 
  Bartók Dávid
  mérnökinformatikus
  nappali

konzulens

• 
  Dr. Mann Zoltán
  egyetemi docens, Számítástudományi és Információelméleti Tanszék

helyezés