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

Budapesti M˝ uszaki és Gazdaságtudományi Egyetem Villamosmérnöki és Informatikai Kar

SAT-solverek gyors´ıtása best-first search algoritmussal

Bartók Dávid II. évfolyam, mérnök informatikus szak

´ am Konzulens: Dr. Mann Zoltán Ad´ Szám´ıtástudományi és Információelméleti Tanszék

2013. október 25.

Tartalomjegyz´ ek 1. Bevezet´ es 1.1. Témav´ alaszt´ as . . . . . . . 1.2. SAT gyakorlati alkalmaz´ asai 1.2.1. Elektronik´ aban . . . 1.2.2. Genetik´ aban . . . . 1.2.3. Egyéb problém´ ak . . 2. Elm´ eleti h´ att´ er 2.1. Keresési fa . . . . . . . . . 2.2. A best-first search . . . . 2.3. SAT-probléma . . . . . . ´ 2.3.1. Attekint´ es . . . . . 2.3.2. DPLL . . . . . . . 2.3.3. CDCL . . . . . . . 2.3.4. Kitekintés: Parallel

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

6 6 7 7 8 9

. . . . . . . . . . . . . . . . . . SAT

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

10 10 11 14 14 15 16 18

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

20 20 20 21 22

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . meghatározása . . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

24 24 24 25 26 26 27 28 29 31

3. Haszn´ alt programok 3.1. MiniSat . . . . . . . . . . . 3.1.1. A cnf form´ atum . . 3.2. SAT-probléma gener´ atorok 3.3. BCAT . . . . . . . . . . . .

. . . . .

. . . .

. . . .

4. Az algoritmus 4.1. Logikai szint . . . . . . . . . . . . . . . . . . . 4.1.1. Az alap¨ otlet . . . . . . . . . . . . . . . 4.1.2. A keresési tér szétosztása . . . . . . . 4.1.3. A heurisztika . . . . . . . . . . . . . . 4.2. Implement´ aci´ o . . . . . . . . . . . . . . . . . 4.2.1. Az eredeti MiniSat m˝ uködése . . . . . 4.2.2. Inicializ´ al´ as . . . . . . . . . . . . . . . 4.2.3. Az assumption¨ okben szerepl˝o változók 4.2.4. A keresés . . . . . . . . . . . . . . . . 5. M´ er´ esek

33

6. Befejez´ es 6.1. Eredmények . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.2. Egyéb ¨ otletek . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

37 37 37

2

´ ak jegyz´ Abr´ eke 1.1. A nehéz fark´ u eloszl´ as . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1. 2.2. 2.3. 2.4. 2.5. 2.6. 2.7.

Visszalépéses keresés . . . . . Best-first search . . . . . . . . Solverpéld´ anyok a f´ aban . . . Szemantikus fa . . . . . . . . Egy megoldhatatlan probléma Az implik´ aci´ os gr´ af . . . . . . A vezet˝ o utak . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . keresési fája . . . . . . . . . . . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

10 12 12 14 14 17 18

3.1. Egy latin négyzet . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2. A probléma nehézségének alakulása . . . . . . . . . . . . . . . . . . . . . . . . . . . .

21 22

4.1. Best-first search 2 solverrel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2. 8 solver megval´ os´ıt´ asa assumptionökkel . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3. A solver sz´ ama és a hozz´ a tartozó assumption-tömb . . . . . . . . . . . . . . . . . .

24 25 29

5.1. 5.2. 5.3. 5.4.

33 34 35 36

A best-first search v´ altozatok eredményei . . . . . . . Az u ´jraind´ıt´ asokkal gyors´ıtott BFS . . . . . . . . . . . A BFS és a MiniSat sz´ or´ asának összehasonl´ıtása . . . Sz´ or´ asok alakul´ asa pr´ımtényez˝ore bontás-problémákon

3

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

. . . .

. . . . . . .

6

. . . .

. . . .

Bart´ ok D´ avid


¨ Osszefoglal´ as A mérn¨ oki gyakorlatban a legfontosabb problémák jelent˝os részére igaz, hogy jelenleg nem létezik minden péld´ anyukat gyorsan (polinomid˝oben) megoldani képes algoritmus. Ezeket összefoglal´ o néven NP-teljes problém´ aknak nevezz¨ uk. Az els˝o ismert NP-teljes probléma a Boolean Satisfiability (SAT), ahol egy logikai formula változóinak próbálunk u ´gy értéket találni, hogy a kifejezés igazra értékel˝ odj¨ on ki. Az ipari alkalmaz´ asokban gyakran fordulnak el˝o 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´ as´ at is keményen pr´ ob´ ara teszi. A kutatása éppen emiatt népszer˝ u, olyannyira, hogy évente SAT-versenyt is rendeznek. Itt saj´ at kész´ıtés˝ u algoritmusokkal lehet részt venni, és a cél problémapéldányok minél gyorsabb megold´ asa. A jelenlegi SAT-megold´ o algoritmusok (solverek) legnagyobb problémája az, hogy bár sok esetben gyorsan oldj´ ak meg a problém´ akat, néha a futási id˝o a szokásosnál nagyságrendekkel hosszabbra is ny´ ulhat. Ennek cs¨ okkentésére a jelenlegi leghatékonyabb módszer az, hogy a keresést bizonyos id˝ ok¨ oz¨ onként u ´jraind´ıtjuk. Val´ osz´ın˝ us´ıthet˝o, hogy ekkor hamarabb eredményre jutunk, mintha az algoritmust beavatkoz´ as nélk¨ ul futtatnánk. Ez a megoldás azonban közel sem tökéletes: a keresés elért részeredményei az u ´jraind´ıt´ asnál elvesznek, valamint semmi sem garantálja, hogy az u ´j futtat´ asn´ al val´ oban gyorsan eredményt kapunk. A TDK dolgozatomban az u ´jraind´ıtás helyett egy másik módszert alkalmazok a futásid˝ok sz´ or´ as´ anak cs¨ okkentésére. Ez a legjobbat el˝oször” (best-first search) algoritmus, amely a fut´ asa ” sor´ an gy˝ ujt¨ ott adatok alapj´ an próbálja kitalálni, merre kell keresn¨ unk a megoldás minél hamarabbi eléréséhez. Ez´ altal a solver képes lesz arra, hogy változtasson a keresési stratégiáján, de az addigi részeredményei megtart´ asa mellett. A jelenlegi SAT-solverek nem o¨sszeegyeztethet˝ok a hagyományos best-first search kialak´ıtás´ aval, ezért az alkalmaz´ ashoz az algoritmus jelent˝os módos´ıtására volt sz¨ uksé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´ an a kész algoritmust a MiniSatba, egy gyors, de könnyen b˝ov´ıthet˝o SAT-solverbe implementáltam. Az eredmények kiértékelését és a finomhangolást egy algoritmusok tesztelését seg´ıt˝o szoftvercsomag, a BCAT k¨ onny´ıtette meg. A tesztelés sor´ an kapott eredmények azt mutatják, hogy ezzel a módszerrel számottev˝ oen gyors´ıtottam a k¨ ul¨ onféle problémapéldányok megoldását, és siker¨ ult csökkentenem a futásid˝ ok hatalmas k¨ ul¨ onbségét is.

4

Bart´ ok D´ avid


Abstract For most of the problems in engineering practice currently exists no algorithm, that can solve all instances quickly (in polynomial time). These problems are called NP-complete. The first known NP-complete problem was Boolean Satisfiability (SAT), in which we have to assign values to the variables of a Boolean formula so that it evaluates to true”. Problems that can easily be interpreted ” as SAT occur often in industrial applications. The difficulty of these can be challenging even for the computational capacity of today’s hardware. Accordingly, the research of this problem is so popular that a SAT competition is held annually. Here the participants apply with self-made algorithms and the goal is to solve many instances of SAT as fast as possible. The greatest trouble with current SAT algorithms (solvers) is that although they mostly solve the problems fast enough, sometimes running time can stretch to even other orders of magnitude. The current most effective solution to this is restarting search after a given amount of time. By using this strategy we probably receive a result faster than if we ran the algorithm without external intervention. However, this method is far from perfect: partial solutions are lost during restarts and we have no guarantee that the next run truly provides a quick result. In this paper I propose another solution to reduce the variance of running times. This is the best-first search algorithm, which uses data collected during its run to predict where the result might be found. Thus the solver becomes able to change its search strategy but also keeping the already discovered partial results. Current SAT solvers are not suited for the usage of best-first search, therefore, significant changes had to be executed on the original algorithm before realization. It was also really important to determine how to approximate the closeness of a solution during search. After the design was complete I implemented the algorithm into MiniSat, which is an effective but easily extensible SAT solver. The evaluation of results and fine-tuning were made easier by BCAT, a software package built for testing of combinatorial algorithms. The achieved results show that by using best-first search I made the solution of several SAT instances significantly faster and the variance of running times has also been reduced.

5

1. fejezet

Bevezet´ es 1.1.

T´ emav´ alaszt´ as

A TDK dolgozatomban a best-first search (BFS) algoritmus alkalmazását mutatom be boolean satisfiability (SAT) problém´ akra. A SAT-problémában egy konjunkt´ıv normálformában megadott logikai formul´ ar´ ol kell eld¨ onten¨ unk, hogy a változóinak tudunk-e u ´gy értéket adni, hogy a kifejezés igazra értékel˝ odj¨ on ki. Ez volt az els˝o ismert NP-teljes probléma: ez azt jelenti, hogy jelenleg nincsen olyan solver (megold´ oprogram), amelyik minden egyes problémapéldányra az input hossz´ anak f¨ uggvényében polinom fut´ asi idej˝ u [12]. Valósz´ın˝ us´ıthet˝o, hogy ilyet egyáltalán nem lehet tal´ alni, azaz csak a probléma egyes speciális példányaira léteznek hatékony algoritmusok. Mivel a SAT´ probléma alkalmaz´ asai szerte´ agaz´ oak, nagyon sokan foglalkoznak a kutatásával. Evente ker¨ ul megrendezésre a nemzetk¨ ozi SAT verseny, ahol saját kész´ıtés˝ u solverekkel lehet nevezni, és a cél k¨ ul¨ onféle problémapéld´ anyok minél gyorsabb megoldása. A SAT-solvereknél jelenleg a legnagyobb probléma az algoritmusok futási idejének u ń. nehéz fark´ u eloszl´ asa (heavy-tailed runtime distribution). Ez azt jelenti, hogy átlagos esetben rövid id˝ o alatt lefut az algoritmus, azonban nem elhanyagolható azon esetek száma, amikor a futási id˝ o az atlag ak´ ´ ar t¨ obbsz¨ or¨ osére is ny´ ulik, vagy néha nagyságrendekkel nagyobbra is. Ez látható az 1.1. abr´ ´ an. Előfordulás gyakorisága

Futási idő

1.1. ábra. A nehéz fark´ u eloszlás

6

Bart´ ok D´ avid


Ennek jelenlegi leghatékonyabb megoldása az, hogy ha az algoritmus már régen fut, akkor u ´jraind´ıtjuk [9]. Ezt azért tessz¨ uk, mert remélj¨ uk, hogy következ˝o nekifutásra másképp fog viselkedni, és eredményesebb lesz, azaz az átlagos futási id˝o alatt, vagy annak környékén végez. Ezzel a megk¨ ozel´ıtéssel t¨ obb probléma is felmer¨ ul: egyrészt az u ´jraind´ıtással elvesznek az algoritmus eddig elért részeredményei. M´ asrészt a statisztikán k´ıv¨ ul semmi sem garantálja, hogy az ismételt pr´ ob´ alkoz´ as gyorsabb lesz. Azonban a gyakorlat azt mutatja, hogy ez az u ń. restart-m´ odszer meglep˝ oen j´ ol m˝ uk¨ odik, és nagy mértékben gyors´ıtja a solverek m˝ uködését [13]. Mi lenne viszont akkor, ha a restart helyett valahogy elérhetnénk azt, hogy az algoritmus valami annyira sz´ amottev˝ ot v´ altoztasson a keresésben, ami felér ugyan egy u ´jraind´ıtással, de emellett megtartan´ a az eddigi eredményeit? K´ıvánatos lenne továbbá az is, hogy a solver ne egy véletlenszer˝ uu ´ton folytassa tov´ abb a keresést, hanem u ´gy, hogy minél nagyobb valósz´ın˝ uséggel jusson gyors megold´ asra. Ezekre a problém´ akra kerestem a megoldást a kutatásom során, azt várva, hogy ´ıgy gyors´ıtani tudom a SAT-solverek m˝ uk¨ odését, legink´ abb a nehézfark´ u eloszlás farokrészének csökkentésén kereszt¨ ul. Ez a cél apr´ obb algoritmikus módos´ıtások seg´ıtségével nem érhet˝o el, ezért egy teljesen u ´j megk¨ ozel´ıtésre volt sz¨ ukségem. A tapasztalatok azt mutatják, hogy a best-first search, melyet a k¨ ovetkez˝ okben részletesen bemutatok, sikeresen alkalmazható ezen célok elérésére a gráfsz´ınezés esetén [5], ami szintén egy NP-teljes probléma. Ez keltette fel a figyelmemet a módszer iránt. A kutat´ asom a k¨ ovetkez˝ o lépésekb˝ol állt: el˝oször áttanulmányoztam a SAT problémához és a best-first searchh¨ oz kapcsol´ od´ o elméleti alapokat. Ezután megismerkedtem a MiniSattal, egy nagyon sikeres SAT-solverrel [7]. Sikerének az oka többek között átláthatóságában és b˝ov´ıthet˝oségében rejlik. Ezut´ an kital´ altam, hogyan lehetne ebbe beép´ıteni a BFS algoritmust, majd kiegész´ıtettem a MiniSat forr´ ask´ odj´ at ennek megfelel˝oen. Az algoritmus tesztelésének megkönny´ıtéséhez implement´ altam azt a BCAT keretrendszerbe, ami egy algoritmusok célirányos tesztelésére szolgáló szoftvercsomag [6]. Az utols´ o lépés a tesztelés és az eredmények értékelése volt.

1.2.

SAT gyakorlati alkalmaz´ asai

A SAT-probléma nagyon fontos szerepet tölt be a mérnöki gyakorlatban. Többféle tervezési és tesztelési feladatban haszn´ alnak SAT-solvereket, valamint számtalan matematikai és informatikai kérdés fogalmazhat´ o meg SAT-problémaként [15]. Ezek köz¨ ul mutatok be néhányat.

1.2.1.

Elektronik´ aban

A kombin´ aci´ os ekvivalencia ellen˝ orzésénél (combinational equivalence checking) azt ellen˝orizz¨ uk, hogy két kombin´ aci´ os h´ al´ ozat azonosan m˝ uködik-e. A gyakorlatban ez például akkor fordulhat el˝ o, hogyha van egy hardver¨ unk, amit már tesztelt¨ unk, és tökéletesen m˝ uködik, de valamilyen okb´ ol apr´ obb m´ odos´ıt´ asokat kell rajta végrehajtanunk. A m˝ uködésen nem szeretnénk változtatni, ezért osszevetj¨ ¨ uk azt az eredeti v´ altozatéval, mivel arról tudjuk, hogy a k´ıvánt kimenetet áll´ıtja el˝o. A megold´ ast u ´gy kapjuk, hogy az összes lehetséges bemenetre összehasonl´ıtjuk a hálózatok kimenetét. Ha minden egyes alkalommal ugyanazt az eredményt adják, akkor ekvivalensek, ha viszont létezik olyan input, hogy az outputok k¨ ulönböz˝oek, akkor nem azonos a m˝ uködés. Azt, hogy az outputok egyenl˝ oek-e, legkönnyebben egy kizáró vagy (XOR) kapcsolattal tudjuk jellemezni. Legyen a két h´ al´ ozatot le´ıró f¨ uggvény f illetve F. Ha a két hálózat nem ekvivalens, legal´ abb egy x inputra igaz a k¨ ovetkez˝o formula: f (x) ⊕ F (x) = 1 A logikai ´ aramk¨ or¨ ok konjunkt´ıv normálformává való konvertálása ismert [3], ezt alkalmazva a fenti formul´ ara egy SAT-problém´ aval találjuk szemben magunkat. Az integr´ alt ´ aramk¨ or¨ okben k¨ ulönböz˝o hibák léphetnek fel, amelyek kisz˝ urése nagyon fontos. Erre a leggyakrabban haszn´ alt m´ odszer az automatikus tesztminta-generálás (automatic test-pattern

7

Bart´ ok D´ avid


generation - ATPG). Az ´ aramk¨ orben található hibákat a stuck-at modell seg´ıtségével képzelhetj¨ uk el: a hardverben egy ¨ osszek¨ ottetés beragadt” valamilyen logikai állapotba (0 vagy 1). Az ATPG ” olyan inputot gener´ al, amivel egyértelm˝ uen kider´ıthet˝o, hogy egy feltételezett hiba jelen van-e a h´ al´ ozatban. Ez a probléma értelmezhet˝ o egy ekvivalencia-ellen˝orzésként is, ahol a két összehasonl´ıtand´ o h´ al´ ozat a j´ ol és a rosszul m˝ uk¨ od˝ o változatok. Amelyik bemenetre a két hálózat k¨ ulönböz˝o kimenetet ad, az alkalmazhat´ o a hiba tesztelésére. Ha nincsen ilyen bemenet, akkor a hiba ilyen m´ odon nem mutathat´ o ki. A gyakorlatban ezt a módszert még k¨ ulönféle tr¨ ukkökkel gyors´ıtják, pl. a hib´ asan m˝ uk¨ od˝ o h´ al´ ozatot nem ¨ onmag´ aban, hanem az eredetit˝ol való k¨ ulönbségeivel reprezentálják, azonban ez a SAT-problém´ av´ a konvert´ alhatóságot nem befolyásolja. Egy rendszer ellen˝ orzésénél nagyon fontos szempont, hogy az megfelel-e a specifikáci´ onak. Erre szolg´ al a modellellen˝ orzés (model checking), aminek a kombinációs ekvivalencia ellen˝ orzése tulajdonképpen egy speci´ alis esete, hiszen abban az esetben a specifikáció maga is egy hálózat. A modellellen˝ orzésnél a specifik´ aci´ ot egy id˝o-logika seg´ıtségével adjuk meg, például a következ˝oképpen: A h˝ ut˝ oben a l´ ampa nem kapcsol fel, am´ıg az ajtó zárva van. NOT lampa bekapcsol UNTIL ajto zarva Ezt a specifik´ aci´ ot hasonl´ıtjuk össze az állapotgépként megadott implementációnkkal. Gyakran defini´ alunk egy ellen˝ orz˝ o f¨ uggvényt, amelynek az állapotgép minden állapotában igaznak kell lennie. Korl´ atozott modellellen˝ orzésnek (bounded model checking) h´ıvjuk azt, amikor azt vizsg´ aljuk, hogy a kezd˝ o´ allapotb´ ol k lépéssz´ ammal milyen állapotokba lehet eljutni, és ezekben az állapotokban teljes¨ ul-e ez a f¨ uggvény. A teszteléshez célszer˝ u ezt 0-tól egy elég nagy k számig végignézni. A modellellen˝ orzés ezen v´ altozata konvertálható SAT-problémává, és a gyakorlatban ez elég hatékonynak bizonyul [2].

1.2.2.

Genetik´ aban

A haplot´ıpusok az ember génkészletében bizonyos genetikai mutációkat tárolnak, ´ıgy a meghat´ aroz´ asuk hasznos lehet k¨ ul¨ onböz˝o betegségek kisz˝ urésére. A haplot´ıpusokat azonban direkt m´ odon nem tudjuk vizsg´ alni, ezért az ember genetikai felép´ıtéséb˝ol (genot´ıpus) határozzuk meg oket statisztikai adatok alapj´ ˝ an. A probléma matematikai le´ır´ asa [14]: Adottak a genot´ıpusok: n darab karakterlánc a {0, 1, 2} számokból, amelyek mindegyike m karakterb˝ ol ´ all. A haplot´ıpusok szintén m hossz´ u karakterláncok, de csak a {0, 1} számokból állhatnak. Két haplot´ıpus (h1 , h2 ) megmagyar´ az egy g genot´ıpust, ha minden 0 < j ≤ m helyiértékre teljes¨ ul a k¨ ovetkez˝ o: Ha gj = 0, akkor h1j = h2j = 0 Ha gj = 1, akkor h1j = h2j = 1 Ha gj = 2, akkor h1j 6= h2j Péld´ aul a 0011 genot´ıpust megmagyarázzák a {0011 és 0011} haplot´ıpusok, a 0122 genot´ıpust a {0101 és 0110} vagy a {0100 és 0111} haplot´ıpusok. A feladatunk egy olyan minimális számosság´ u haplot´ıpus-halmazt találni, amelyb˝ol minden genot´ıpushoz ki tudunk v´ alasztani 2 (nem feltétlen¨ ul k¨ ulönböz˝o) elemet u ´gy, hogy a kiválasztott elemek megmagyar´ azz´ ak a genot´ıpust. 8

Bart´ ok D´ avid


Az 1.1. t´ abl´ azatban egy 4 darab, 4 karakter hossz´ u genot´ıpusból álló példán szemléltetem a problém´ at. A t´ abl´ azat azt is tartalmazza, hogy az egyes genot´ıpus milyen haplot´ıpus-párokkal magyar´ azhat´ o meg. Genot´ıpus 0011 0101 0002 2012

Haplot´ıpus 1 0011 0101 0000 0010 0011

Haplot´ıpus 2 0011 0101 0001 1011 1010

1.1. táblázat. Haplot´ıpus meghatározás A f´ elk¨ ov´ errel jel¨ olt haplot´ıpusokat mindenképpen bele kell választanunk a halmazba, mert az els˝ o h´ arom genot´ıpust csak vel¨ uk magyarázhatjuk meg. Így a 0011, amit már a halmazba v´ alasztottunk, az 1010 -val egy¨ utt megmagyarázza az összes genot´ıpust. Ezzel megtaláltuk a minim´ alis halmazt. Természetesen ez egy nagyon egyszer˝ u problémapéldány, bonyolultabb problém´ ak esetén viszont kifizet˝ od˝ o a SAT-problémává konvertálás és az ´ıgy történ˝o megoldás.

1.2.3.

Egy´ eb probl´ em´ ak

Nagyon sok feladat megfogalmazható SAT-problémaként, ezek köz¨ ul csak párat sorolok fel: • Gr´ afsz´ınezés: Kisz´ınezhet˝ oek-e egy gráf cs´ ucsai k darab sz´ınnel u ´gy, hogy a szomszédos cs´ ucsok k¨ oz¨ ott ne legyen azonos sz´ın˝ u? • Integer linear programming (ILP): Adott valahány egészérték˝ u változó, és line´ aris egyenl˝ otlenségek, amelyeknek teljes¨ ulnie kell. A feladat egy adott, a változókból álló line´ aris célf¨ uggvény maximaliz´ al´ asa. • Klikk probléma: Egy gr´ afban maximális méret˝ u teljes részgráf keresése. • Pr´ımtényez˝ okre bonthat´ os´ ag: Egy adott számról el kell dönten¨ unk, hogy pr´ım-e.

9

2. fejezet

Elm´ eleti h´ att´ er 2.1.

Keres´ esi fa

Keresési f´ anak egy olyan f´ at nevez¨ unk, amely rendelkezik egy kit¨ untetett cs´ uccsal (gyökér), amib˝ ol elindulunk a keresés sor´ an, illetve a fa levelei lehetséges megoldásokat reprezentálnak, amelyek k¨ oz¨ ul tetsz˝ oleges mennyiség˝ u lehet val´ oban megoldás. Természetesen az is el˝ofordulhat, hogy egyetlen megold´ as sem létezik. A bej´ ar´ as során a kiindulási cs´ ucsból a levelek felé haladunk, azonban ez t¨ obbféleképpen is megval´ os´ıthat´ o az elágazások miatt. A keresés során tehát minden cs´ ucsban d¨ ontéseket kell hoznunk arr´ ol, hogy merre k´ıvánunk továbbhaladni. Ezeket a döntési lehet˝oségeket jelentik a cs´ ucsokat ¨ osszek¨ ot˝ o élek. A fa cs´ ucsai a gy¨ okért˝ ol val´ o t´ avolság szerint szinteken helyezkednek el: a fa tetejéb˝ol indulunk a keresésnél, és a legals´ o szinten helyezkednek el a levelek. A fa szintjeit azzal azonos´ıtjuk, hogy h´ any d¨ ontés ut´ an jutunk el r´ ajuk. Ez alapján a fa gyökere a 0. szintnek tekinthet˝o. A legegyszer˝ ubb algoritmus ilyen problémák megoldására az, ha elindulunk lefelé a f´ aban, véletlenszer˝ uen el´ agazva minden egyes szinten. Ha egy olyan cs´ ucshoz jutunk el, ami ellentmond´ asra vezet, akkor visszalép¨ unk a legutolsó olyan pontba, ahol még egyéb irányba is elágazhatunk, majd erre folytatjuk a keresést. Ez a visszalépéses keresés (backtrack search), ami tulajdonképpen a mélységi kereséshez hasonl´ oan j´ arja be a fát. (0)

(1)

(. . . )

(2) (3) ø

(4) ø

(5) (6) X

(. . . )

(. . . ) ø

(. . . ) ø

(. . . ) X

(. . . ) (. . . ) ø

(. . . ) ø

2.1. ábra. Visszalépéses keresés A 2.1. ´ abr´ an l´ athat´ o az algoritmus m˝ uködése. A számok azt jelentik, hogy a backtrack milyen sorrendben l´ atogatja meg a fa egyes cs´ ucspontjait, az alsó szint alatti áth´ uzott kör azt, hogy az adott cs´ ucs nem megold´ as, a pipa pedig megoldást jelez. Az els˝o konfliktus a 3. lépés után történt, ahonnan az algoritmus visszaugrott a 2. cs´ ucsra. A 4. lépésben ismét konfliktus történt, ezért az 1. cs´ ucsba tért¨ unk vissza. Itt vég¨ ul az 5. cs´ ucson kereszt¨ ul a 6. lépéssel megtaláltuk a megold´ ast. 10

Bart´ ok D´ avid


A . . . -tal jel¨ olt cs´ ucsokat az algoritmus nem látogatta meg. Mivel a backtrack az els˝o megold´ as megtal´ al´ asa ut´ an kilép, a m´ asik megoldást nem fedezt¨ uk fel. A visszalépéses keresés egy egzakt algoritmus, ami azt jelenti, hogy garantáltan helyes v´ alaszt ad a problém´ ara. A véletlenszer˝ u elágazások miatt természetesen ugyanazon a problém´ an is el˝ ofordulhatnak eltérések a fut´ asid˝oben többszöri futtatás esetén. Az algoritmus rekurz´ıv megval´ os´ıt´ as´ at az al´ abbi pszeudok´ od ´ırja le: 1 2 3 4 5 6 7 8 9 10 11 12 13 14

BTSearch(Problem P, Assignment A) { for(d=firstDecision; d<=lastDecision; d++) A=addDecision(A, d); if(NOT(contradiction(P, A)) if(solved(P, A)) return true; else if (BTSearch(P, A) == true) return true; else A=undoDecision(A, d); return false; } • Problem P: Az adott probléma. • Assignment A: Az eddig meglev˝o döntések listája, a legels˝o f¨ uggényh´ıváskor ez u ¨res. • firstDecision, lastDecision: A döntéseket egész számokként elképzelve az els˝o és utols´ o lehetséges értékek. • addDecision(): Egy adott d¨ ontést hozzáad az aktuális döntések listájához. • contradiction(): Igaz értéket ad vissza, ha talált ellentmondást az adott döntési lista alapj´ an. • solved(): Igaz értéket ad vissza, ha az adott döntések megoldást adnak a problémára. • undoDecision(): Visszavonja a döntési lista legutolsó döntését, azaz egy szinttel feljebb ker¨ ul¨ unk a keresési f´ aban.

2.2.

A best-first search

A best-first search a visszalépéses kereséssel ellentétben nem a mélységi keresésre ép¨ ul, hanem mindig a feladat szempontj´ ab´ ol leg´ıgéretesebbnek t˝ un˝o csomópontot fejti ki. Erre egy kiértékel˝o heurisztikus f¨ uggvényt haszn´ al, ami a csom´ opontokhoz egy számot rendel azok tulajdonságai alapján. Ha ez a f¨ uggvény azt pr´ ob´ alja k¨ ozel´ıteni, hogy a keresési fában mennyire vagyunk közel a megoldáshoz, moh´ o best-first search algoritmusr´ ol beszél¨ unk. A 2.2. ´ abr´ an azt l´ athatjuk, amint az algoritmus az els˝o lépés után u ´gy ´ıtéli meg, hogy a lentebb lépés helyett kedvez˝ obb, ha ink´ abb a másik azonos szinten lev˝o döntést fejti ki. Ezután azonban mégis ´ıgéretesebbnek t˝ unik az els˝ o döntésb˝ol továbblépés (3. cs´ ucs). A következ˝o, 4. lépésben meg is tal´ aljuk a megold´ ast. Ezen az egyszer˝ u péld´ an is l´ athatjuk az algoritmus f˝obb jellegzetességét: ahelyett, hogy csak ellentmond´ as esetén lépne vissza, minden egyes döntés után mérlegeli, hogy hol érdemes folytatni a keresést. A 2. lépés természetesen nem a legjobb döntés, hiszen egyb˝ol is megtalálhattuk volna a megold´ ast. Annak az oka, hogy mégis itt folytattuk a keresést az, hogy a csomópontokat kiértékel˝ o 11

Bart´ ok D´ avid


(0)

(1)

(2) (3)

(. . . ) (. . . ) ø

(. . . ) ø

(4) X

(. . . )

(. . . )

(. . . ) ø

(. . . ) ø

(. . . ) X

(. . . ) ø

(. . . ) ø

2.2. ábra. Best-first search f¨ uggvény csup´ an megbecs¨ ulni tudja a megoldás közelségét. A visszalépéses kereséshez hasonl´ oan ez az algoritmus is egzakt, a kiértékel˝o f¨ uggvény csak az algoritmus futásidejét befolyásolja, de a bej´ ar´ as ugyan´ ugy mindig j´ o eredményt fog adni. A best-first search a gyakorlatban u ´gy is megvalós´ıtható, hogy a keresési fát diszjunkt részekre osztjuk, és ezek mindegyikében létrehozunk egy-egy solverpéldányt. A keresés során ezek k¨ oz¨ ott v´ altogatunk az alapj´ an, hogy melyik t˝ unik a legsikeresebbnek. Ebben a változatban már nem feltétlen¨ ul mérlegelj¨ uk minden lépés után, hogy melyik solvert futtassuk, hanem csak bizonyos id˝ ok¨ oz¨ onként ker¨ ul sor a kiértékel˝o f¨ uggvény használatára. Így jelent˝osen csökkenthet˝o a heurisztik´ aval kapcsolatos j´ arulékos er˝ oforrásköltség (overhead). (. . . )

(. . . )

1. solver

(. . . )

2. solver

3. solver

4. solver

2.3. ábra. Solverpéldányok a fában A 2.3. ´ abr´ an l´ athat´ o ennek az alapötlete: u ´gy hozhatunk létre a legegyszer˝ ubben diszjunkt részeket a f´ aban, hogy a solverek kiindulópontjának egy, az eredetihez képest lentebbi szintet v´ alasztunk. Az ezen a szinten lev˝o minden egyes cs´ ucsból el kell ilyenkor ind´ıtanunk egy solvert, k¨ ul¨ onben nem fedj¨ uk le az egész keresési teret. A fenti példában négy részre osztottuk a fát, ennek megfelel˝ oen a 2. szintr˝ ol kezdj¨ uk a keresést. Az alábbi pszeudokód a best-first search megvalós´ıt´ as´ at ´ırja le:

12

Bart´ ok D´ avid

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19


BFSSearch(List L) { Solver currentSolver=firstOfList(L); while(true) currentSolver.assignment=addDecision(currentSolver); markNode(currentSolver.assignment); if(solved(currentSolver)) return true; if(contradiction(currentSolver)) if(exhausted(currentSolver)) removeFromList(L, currentSolver) if(isEmpty(L)) return false; else undoDecision(currentSolver); if(”limit for running the current solver is reached” OR ”current solver was exhausted”) currentSolver.heuristic=setHeuristic(currentSolver); currentSolver=findMaxHeuristic(L);

20 21

} • List L: A keresésre haszn´ alt solverek listája. • Solver currentSolver: Az éppen futtatott solver, tagváltozói: assignment: Aktu´ alis d¨ ontési lista. heuristic: Mennyire j´ ar közel a solver a megoldáshoz. • firstOfList(): Visszaadja egy lista els˝o elemét. • addDecision(): Megvizsg´ alja a problémát és a döntések meglev˝o listáját, majd egy u ´j d¨ ontést hoz létre. • markNode(): R¨ ogz´ıti, hogy az adott cs´ ucsát meglátogattuk a fának. • exhausted(): Igaz értéket ad vissza, ha a solver már teljes egészében bejárta a keresési tér neki sz´ ant részét. • removeFromList(): Elt´ avol´ıtja a solvert a listából. • isEmpty(): Igaz értéket ad vissza, ha u ¨res a lista, ez azt jelenti, hogy a probléma megoldhatatlan. • setHeuristic(): Kiértékel˝ o f¨ uggvény, amely az adott probléma és a döntések alapján pr´ ob´ alja meghat´ arozni, hogy mennyire vagyunk közel a megoldáshoz. • findMaxHeuristic(): A solverek listájából kiválasztja azt, amelyiket legközelebb érdemes futtatnunk.

13

Bart´ ok D´ avid

2.3. 2.3.1.


SAT-probl´ ema ´ Attekint´ es

Adott egy logikai formula (F) konjunkt´ıv normálforma alakban. A probléma a következ˝o: tudunk-e a v´ altoz´ oknak u ´gy értéket adni, hogy F igaz lesz? A probléma megértéséhez sz¨ ukség¨ unk van néhány defin´ıcióra [8]: Liter´ al: Egy v´ altoz´ o vagy annak negáltja. Kl´ oz: Liter´ alok diszjunkci´ oja. Konjunkt´ıv norm´ alforma: Kl´ ozok konjunkciója. Interpret´ aci´ o: Egy formula minden egyes változójához értéket rendel¨ unk. Egy n változób´ ol ´ all´ o formul´ anak pontosan 2n darab k¨ ulönböz˝o interpretációja van. A formula interpret´ aci´ oit ´ abrázolhatjuk szemantikus fa formájában (2.4. ábra). Itt teh´ at l´ athatjuk, hogyan is néz ki a SAT-probléma esetében a keresési fa: az elágazások az egyes változ´ oknak adott értékek alapj´ an j¨ onnek létre. Kiindulás

x0 =0 x1 =1

x1 =0 x2 =0

x0 =1

x2 =1

x2 =0

x1 =1

x1 =0

x2 =1

x2 =0

x2 =1

x2 =0

x2 =1

2.4. ábra. Szemantikus fa Ezt a keresési f´ at kell bej´ arnunk a solver seg´ıtségével. Ha találunk egy olyan levelet, ahol az adott interpret´ aci´ ot kiértékelve a formula igaz lesz, megtaláltuk a megoldást (satisfiable). A solverek hatékonys´ ag´ at mutatja az, hogy mennyire hamar találják meg a fa ezen pontját. Ha a levelek k¨ oz¨ ul egyik sem ad megoldást, akkor a probléma megoldhatatlan (unsatisfiable). Ennek ellen˝ orzéséhez legrosszabb esetben mind a 2n levelet be kell járnunk, ami exponenci´ alisan sok lépést jelent. Legt¨ obbsz¨ or azonban nincsen sz¨ ukség az összes lépés végrehajtására: ha m´ ar a fa legals´ o szintje el˝ ott ellentmondásra akadunk, azzal egész ter¨ uleteket zárhatunk ki a keresésb˝ ol. Ennek magyar´ azata, hogy ha m´ ar néhány változó adott értékei ellentmondásra vezetnek, ez nem oldhat´ o fel u ´jabb v´ altoz´ oknak t¨ ortén˝o értékadással. (0)

(1) (2) (3) ø

(4) ø

(6) (5) (. . . ) ø

(7)

(. . . ) ø

(8) ø

(9) ø

(10) (11) ø

(12) ø

2.5. ´ abra. Egy megoldhatatlan probléma keresési fája

14

Bart´ ok D´ avid


Az 2.5. ´ abr´ an péld´ aul m´ ar az 5. lépésben észrevett¨ uk a keresésnél, hogy a cs´ ucs alatt lev˝o levelek k¨ oz¨ ul egyik sem megold´ as.

2.3.2.

DPLL

A SAT-probléma kapcs´ an a kl´ ozok le´ırására a következ˝o defin´ıciókat használjuk: Satisfied kl´ oz: Olyan kl´ oz, amelynek legalább egy literálja igaz értéket kapott. Unsatisfied kl´ oz: Olyan kl´ oz, amelynek már összes literálja hamis értéket kapott. Unit kl´ oz: Olyan kl´ oz, amelyben már egy kivételével minden literálnak van értéke, de ezek mindegyike hamis. Unresolved kl´ oz: Amikor a kl´ ozra a fenti állapotok köz¨ ul egyik sem teljes¨ ul. Az egyszer˝ ubb felép´ıtés˝ u SAT-solverek a DPLL (Davis–Putnam–Logemann–Loveland) [4] algoritmusra ép¨ ulnek. Ez tulajdonképpen a fentebb részletezett backtrack egy kiegész´ıtett változata. A legfontosabb kiegész´ıtés a unit propagation: minden értékadás után észleli a unit klózokat, és a k¨ ovetkez˝ o értékad´ as ez alapj´ an t¨ orténik. Ennek oka, hogy a unit klóz utolsó literáljának igaz értéket kell adnunk, hogy a kl´ oz satisfied legyen. Néh´ any DPLL algoritmus tartalmazza az u ń. pure literal rule-t is: Ha egy változó vagy csak pon´ altan, vagy csak neg´ altan szerepel az egész kifejezésben, a keresés legelején megkapja els˝o esetben az igaz, m´ asodik esetben a hamis értéket, hiszen ´ıgy az összes ezt tartalmazó klóz satisfied lesz. Ezeket a kl´ ozokat a kés˝ obbi keresés során nem kell figyelembe venni. A DPLL legegyszer˝ ubb megval´ os´ıt´ asa a backtrackhez hasonlóan rekurz´ıvan történik, ezt szemlélteti a következ˝o pszeudok´ od is: 1 2 3 4 5

Solve(Problem P) { A=assignPureLiterals(P); return DPLL(P, A); }

6 7 8 9 10 11 12 13 14 15 16 17 18

DPLL(Problem P, Assignment A) { unitPropagate(P, A); if(contradiction(P,A)) return false; if(allVariablesAssigned(P,A)) return true; variable V=chooseVariable(P, A); newAssignment1=addDecision(A, V); newAssignment2=addDecision(A, NOT(V)); return( DPLL(P, newAssignment1) OR DPLL(P, newAssigment2)); } • unitPropagate(): A unit kl´ ozokban fennmaradó változóknak értéket ad. Ha ennek sor´ an u ´j unit kl´ oz keletkezik, akkor a folyamat tovább folytatódik. • assignPureLiterals(): A csak egyféle polaritással szerepl˝o változóknak rögtön értéket ad. • allVariablesAssigned(): Ellen˝orzi, hogy minden változónak van-e már értéke. Mivel a konfliktusokat az ez el˝ otti f¨ uggvényh´ıvással már kisz˝ urt¨ uk, a visszaadott igaz érték egy jó megold´ ast jelez.

15

Bart´ ok D´ avid


• chooseVariable(): A probléma és az eddigi döntések alapján kiválasztja a következ˝o változ´ ot, aminek értéket adunk.

2.3.3.

CDCL

A CDCL (conflict-driven clause learning) a modern solverek által leggyakrabban használt algoritmus. Az el˝ oz˝ o fejezetben ismertetett DPLL-re ép¨ ul, de azt jelent˝os módos´ıtásokkal használja. A legfontosabb k¨ ul¨ onbség, hogy minden konfliktus után egy tanult klóz ker¨ ul hozzáadásra a formulához. A tanult kl´ oz a konfliktushoz vezet˝ o értékadások, vagy ezek egy részének negáltját tartalmazza. Ennek a célja az, hogy elker¨ ulj¨ uk ugyanazon konfliktus kétszeri el˝ofordulását. A keresés sor´ an az értékad´ asokhoz mindig kapcsolunk egy döntési szintet. Ez megadja, hogy a keresés alatt hanyadik d¨ ontéssel kapott értéket a változó. A unit propagation során értéket kapott v´ altoz´ ok nem rendelkeznek saj´ at döntési szinttel, hanem a legutóbbi döntés szintjét kapják meg. xi = v@d xi : az értéket kap´ o v´ altoz´ o v: a kapott érték (1: igaz, 0: hamis) d: az aktu´ alis d¨ ontési szint L´ assuk az el˝ obb bevezetett jelölések használatát és a klóztanulás megvalós´ıtását egy konkrét péld´ an kereszt¨ ul: ω1 = (x1 ∨ x2 ∨ ¬x7 ) ω2 = (¬x3 ∨ x4 ∨ x7 ) ω3 = (¬x5 ∨ ¬x6 ) ω4 = (¬x4 ∨ x5 ) ω5 = (¬x3 ∨ ¬x4 ∨ x6 ) Az eddigi d¨ ontések: x1 = 0@1 x3 = 1@2 A jelenlegi d¨ ontés: x2 = 0@3 Ezek alapj´ an felép´ıtj¨ uk az implikációs gráfot (2.6. ábra), melynek cs´ ucsai a meglev˝o értékad´ asok. Az élek az alapj´ an j¨ onnek létre, hogy melyik értékadásból mi következik; feliratuk azt jelzi, hogy melyik unit kl´ oz felelt a végpontn´ al szerepl˝o értékadásért. Például x7 azért kapott 0 értéket, mert a ω1 kl´ ozban szerepl˝ o x1 és x2 liter´ alok 0 értékéb˝ol adódóan a klóz unittá vált.

16

Bart´ ok D´ avid


x6 = 1@3 ω5

ω5

x3 = 1@2 ω2

x1 = 0@1

x4 = 1@3 ω2

ω1

ω4

x7 = 0@3

x5 = 1@3

ω1

ω3

x2 = 0@3

x6 = 0@3 2.6. ábra. Az implikációs gráf

A gr´ afban felfedezhet˝ o a konfliktus: Az értékadásokból következik, hogy x6 -nak egyszerre kellene 0 és 1 értékkel rendelkeznie. Ez nyilvánvalóan nem lehetséges, ezért az eddig sz¨ uletett döntések mellett a probléma megoldhatatlan. Tehát a három változó köz¨ ul legalább az egyiknek a péld´ aban szerepl˝ ot˝ ol eltér˝ o értéket kell kapnia, hogy ne jussunk ellentmondásra. Ez alapján a következ˝o kl´ ozt tanulhatjuk meg: ωl = (x1 ∨ x2 ∨ ¬x3 ). A tanult kl´ oz teh´ at megakad´ alyozza azt, hogy kétszer ugyanaz a konfliktus forduljon el˝ o. Ez lehet˝ ové teszi, hogy a konfliktus után ne közvetlen¨ ul a legutolsó döntés elé lépj¨ unk vissza, hanem egy feljebb lév˝ o d¨ ontési szintre (non-chronological backtrack). A CDCL a kl´ oztanul´ ast a valóságban nem feltétlen¨ ul az itt bemutatt módszer szerint végzi. Léteznek kifinomultabb megold´ asok [4], amellyel a folyamatot optimalizálni lehet, azonban ezek ismertetését˝ ol most eltekintek, hiszen a best-first search alkalmazásához ezekre nincsen sz¨ ukség. Fontos megeml´ıteni, hogy a CDCL algoritmusban nem tároljuk explicit módon az összes kl´ ozban szerepl˝ o mindegyik liter´ al értékét. Ennek (leegyszer˝ us´ıtve) az az oka, hogy a klózban mindig csak két liter´ al értékét figyelj¨ uk, és ezek alapján következtet¨ unk a klóz állapotára. Ez az u ń. watched literal scheme [17]. Ez az adatstrukt´ ura jelent˝osen gyors´ıtja az algoritmust, ugyanakkor, mint kés˝obb l´ atni fogjuk, sz´ amunkra korl´ atoz´ ast jelent a keresés során elérhet˝o információk tekintetében. A CDCL algoritmusban el˝ oszeretettel alkalmaznak restartokat is, akár a tanult klózok megtart´ asa mellett. Minden egyes u ´jraind´ıt´ asnál n˝o a limit, amit a solvernek a probléma megoldására adunk, hiszen egyébként el˝ o´ allhatna egy olyan helyzet, hogy soha nem jutunk eredményre. Nagy méret˝ u problém´ ak esetén a tanult kl´ ozok száma hatalmas lehet, ilyenkor célszer˝ u a memóriaigényre val´ o tekintettel alkalmanként t¨ or¨ oln¨ unk ezekb˝ol. Az algoritmus f˝obb lépéseit az alábbi iterat´ıv kódrészlet szemlélteti:

17

Bart´ ok D´ avid

1 2 3 4 5 6 7 8 9 10 11 12 13


CDCL(Problem P) { Assignment A=empty; while(true) if (unitPropagation(P, A) == CONFLICT) newDecisionLevel=analyzeConflict(P, A) if(newDecisionLevel<0) return false; else backtrack(P, A, newDecisionLevel); if (allVariablesAssigned == true) return true; (Variable, Polarity)=branchingHeuristic(P, A); addDecision(A, Variable, Polarity);

14 15

} • unitPropagation(): Itt a konfliktusok kisz˝ urésére is szolgál, ha egy változó két unit klóz utols´ o elemeként is szerepel, méghozzá k¨ ulönböz˝o polaritással, akkor ellentmondásra jutottunk. • analyzeConflict(): Az adott konfliktust elemezve visszaad egy döntési szintet, ahova optim´ alis backtrackelni, valamint hozzáad egy tanult klózt a problémához. Ha a visszaadott d¨ ontési szint kisebb, mint 0, a probléma unsatisfiable, hiszen a kiinduló cs´ ucsnál feljebb nem tudunk visszalépni a keresésben. • backtrack(): Visszatér a keresési fa egy adott szintjére, visszavonva az az utáni döntéseket. • branchingHeuristic(): Megadja, hogy mely változónak és milyen értéket célszer˝ u adni.

2.3.4.

Kitekint´ es: Parallel SAT

A t¨ obbmagos processzorok elterjedésével felmer¨ ult az ötlet, hogy a SAT-problémák megoldása u ´gy is gyors´ıthat´ o, ha p´ arhuzamosan több solvert is futtatunk. Erre két f˝obb megoldás létezik [16]: Az els˝ o m´ odszer a keresési tér szétosztása: a módszer lényege, hogy a keresési teret diszjunkt részekre osztjuk, és ezeken futtatjuk a solvereket. Ez a guiding paths (vezet˝o utak) m´ odszer seg´ıtségével t¨ orténik: itt a v´ altoz´ oknak nem csak az adott értékét mentj¨ uk el, hanem azt is, hogy mindkét lehetséges érték¨ uk ki lett-e próbálva a keresés során. Minden egyes olyan változó, amely még csak egyféle értékkel rendelkezett a keresés során, alkalmas arra, hogy a meglev˝o keresési teret két részre osszuk. Ezeket a v´ altoz´ okat nyitottnak nevezz¨ uk. Kiindulás

Kiindul´ as x0 =0

x0 =1

1. solver

2. solver

x0 =0 ...

x0 =1 UNSAT

x5 =0 ...

x5 =1 2. solver

1. solver 2.7. ábra. A vezet˝o utak

18

Bart´ ok D´ avid


A solverek sz´ ama legt¨ obbsz¨ or adott, a 2.7. ábrán például 2. Amikor az egyik solver befejezte a saj´ at ter¨ uletén a keresést (teh´ at unsatisfiable értékkel tért vissza), akkor a keresési fában legfeljebb tal´ alhat´ o nyitott v´ altoz´ on´ al el´ agazik a keresés, és az eddig bejáratlan ter¨ uletet megkapja az éppen tétlen solver. A tanult kl´ ozok minden konfliktus után átadódnak a többi solvernek, azonban a nagy mem´ oriaigény miatt ez csak korl´ atozott számban lehetséges. A m´ asik m´ odszer a portf´ oli´ ok használata. Itt u ´gy használjuk ki a párhuzamos´ıtás adta lehet˝ oségeket, hogy egyszerre futtatunk több solvert a problémán, de k¨ ulönböz˝o paraméterekkel. Eltér˝ oek lehetnek t¨ obbek k¨ oz¨ ott az u ´jraind´ıtás gyakoriságában, a klóztanulás módszerében, vagy az értékad´ asi heurisztik´ aban. Ezek a solverek részben megosztják egymással a tanult klózokat, ´ıgy seg´ıtve egym´ as munk´ aj´ at. Ez elképzelhet˝o u ń. master-slave felép´ıtésben is. A masterek végzik a tényleges keresést, és mindegyiknek van egy saját slave-je, amik megkapják a mastert˝ol a konfliktusok list´ aj´ at, és kifejezetten csak azokon a részeken keresnek, amelyek közelében a masternek konfliktusa volt. A master és a hozzá tartozó slave csak egymással osztják meg a tanult klózokat, és mivel hasonl´ o ter¨ uletet j´ arnak be, ´ıgy ezek egymás számára relevánsabbak, mint véletlenszer˝ u bej´ ar´ asok esetén [11]. Ezek az eredmények sz´ amomra is fontosak voltak a munkám során, annak ellenére, hogy nem alkalmazok direkt m´ odon p´ arhuzamos´ıtást. A fenti módszerek köz¨ ul én is alkalmazom a keresési tér szétoszt´ as´ at, hiszen ez t¨ obb solver létrehozásánál lényeges kérdés. Az én algoritmusom azonban nem futtat egyszerre t¨ obb solvert, hanem azt próbálja meghatározni, hogy az egyetlen futó solver éppen melyik legyen.

19

3. fejezet

Haszn´ alt programok 3.1.

MiniSat

A MiniSat [7] egy ny´ılt forr´ ask´ od´ u, C++-ban ´ırt SAT-solver, amelyet ketten kész´ıtettek el 2003ban. Az els˝ o v´ altozat programk´ odja csupán 600 soros volt, mégis tartalmazta a CDCL solverek osszes jellegzetességét. Célir´ ¨ anyosan arra fejlesztették ki, hogy seg´ıtse a szakter¨ uleten a kutat´ asokat és a fejlesztéseket. Ebb˝ ol ad´ od´ oan jól dokumentált, könnyen átlátható szerkezet˝ u és egyszer˝ uen m´ odos´ıthat´ o. Az u ´jabb verzi´ ok már hosszabb kóddal rendelkeznek, de a solver lényegi része még mindig egy kicsivel kevesebb, mint 1 000 sorból áll. A MiniSat 2005-ben a SAT versenyen 4 kateg´ ori´ aban ért el els˝ o helyet, nagy fölénnyel legy˝ozve versenytársait. Számos kutatás eszközeként bizony´ıtott m´ ar, ezért esett az én választásom is rá. A MiniSat eredetileg Linux alatti használatra kész¨ ult, de a futtatása Windows alatt is megoldhat´ o, azonban ehhez néh´ any Linux specifikus programrész eltávol´ıtása sz¨ ukséges. Ezek a programk´ od-részletek nélk¨ ul¨ ozhet˝ oek a solver m˝ uködéséhez, hiszen csak CPU és memória er˝oforr´ askorl´ atoz´ asokra szolg´ alnak. Innent˝ ol nincs m´ as teend˝ onk, mint futtatni a MiniSatot. A program parancssori argumentumok form´ aj´ aban kapja meg a bemeneti problémát cnf formátumban és a kimeneti txt fájlt, amibe a megold´ as ker¨ ul. Az argumentumok formátuma a következ˝o: minisat.exe [bemeneti f´ ajl neve] [kimeneti f´ ajl neve] [esetleges opci´ ok] A MiniSat az objektumorient´ alt elveket követve kész¨ ult, tehát egy Solver nev˝ u osztály szolg´ al a problém´ ak megold´ as´ ara. Ebben vannak eltárolva a cnf fájlból beolvasott adatok, és a keresés elind´ıt´ asa is egy met´ odus megh´ıvásával történik. Ez a tulajdonság a kutatásom során jelent˝ os szerepet j´ atszott, hiszen ´ıgy egyszer˝ uen lehet több solvert párhuzamosan létrehozni. A program t´ amogatja az u ´gynevezett assumptionök használatát. Ez azt jeleneti, hogy megadhatjuk a solvernek, hogy néh´ any változó adott érték˝ u legyen végig a keresés során, az pedig ezen feltételek mellett pr´ ob´ al megoldást találni. Fontos megjegyezni, hogy ha a solver unsatisfiable eredményre jut, az csup´ an azt jelenti, hogy az adott assumptionök mellett nem létezik megold´ as. Ez a funkci´ o a keresési tér szétosztásánál fog fontos szerepet játszani.

3.1.1.

A cnf form´ atum

A SAT-problém´ ak t´ arol´ asa legt¨ obbször az el˝oz˝o fejezetben is eml´ıtett cnf formátumban történik, melynek felép´ıtése a k¨ ovetkez˝ o:

20

Bart´ ok D´ avid


c Minta p cnf 5 3 1 −5 0 2 3 −1 0 −4 1 2 0 A c-vel kezd˝ od˝ o sorok kommentként tekintend˝ok, a fájl feldolgozása közben lényegi jelent˝oség¨ uk nincs. Az els˝ o val´ oj´ aban feldolgozandó sor tartalma mindig adott: p cnf [v´ altoz´ ok sz´ ama] [kl´ ozok sz´ ama] Ezut´ an k¨ ovetkeznek a kl´ ozok: a változókat számokkal jelölj¨ uk, 1-t˝ol n-ig, ahol a probléma n v´ altoz´ ot tartalmaz. A neg´ alt literálok negat´ıv el˝ojellel szerepelnek. A literálokat egy-egy sz´ ok¨ oz v´ alasztja el, a kl´ oz végét pedig egy 0 karakter jelzi, és általában egy sorban egy klóz találhat´ o. Ezek ismeretében a fenti minta fájl az alábbi problémát kódolja: (x1 ∨ ¬x5 ) ∧ (x2 ∨ x3 ∨ ¬x1 ) ∧ (¬x4 ∨ x1 ∨ x2 )

3.2.

SAT-probl´ ema gener´ atorok

A solverek teszteléséhez nagy mennyiség˝ u SAT-problémára van sz¨ ukség¨ unk, ezek el˝oáll´ıtása azonban nem egyszer˝ u feladat. Az interneten tal´ alhat´ o cnf f´ ajlok szinte mindegyike t´ ul könny˝ u (tizedmásodpercek alatt megoldhat´ o), vagy annyira nehéz, hogy percekig tartó futás után sem jut eredményre a solver. Ezért célszer˝ u SAT-probléma gener´ atort használni, amelyt˝ol alapvet˝o elvárás, hogy tudja szabályozni a problém´ ak nehézségét. Ugyancsak fontos, hogy tegye lehet˝ové k¨ ulön megoldható, illetve nem megoldhat´ o problém´ ak gener´ al´ as´ at. A SAT-problém´ ak gener´ al´ as´ ara a legegyszer˝ ubb módszer, ha adott szám´ u változ´ ob´ ol véletlenszer˝ uen elkezd¨ unk kl´ ozokat gyártani. Az ´ıgy keletkez˝o példányokról azonban nem tudjuk el˝ ore, hogy megoldhat´ oak lesznek-e. Ezt a megoldást tehát nem alkalmazhatjuk, ha csak megoldhat´ o problém´ akon szeretnénk tesztelni. Egy m´ asik m´ odszer az, hogy el˝ore kitalálunk egy megoldást, és a generálásnál csak azokat a kl´ ozokat tartjuk meg, amelyeket ez a megoldás igazzá tesz. Az ´ıgy keletkez˝o problémák mindenképpen megoldhat´ oak lesznek, azonban a gyakorlat azt mutatja [1], hogy ezek a péld´ anyok egyszer˝ ubbnek bizonyulnak a hasonló méret˝ u, de véletlen generáltakkal szemben. Az lsencode [1] egy kifejezetten megoldható SAT-problémák generálására kész¨ ult, C++-ban ´ır´ odott szoftver. A m˝ uk¨ odése legegyszer˝ ubben latin négyzetek seg´ıtségével szemléltethet˝o [10].

1 2 3 4

2 4 1 3

3 1 4 2

4 3 2 1

3.1. ábra. Egy latin négyzet Ezek olyan N ×N méret˝ u t´ abl´ azatok, amelyek N számmal vannak feltöltve u ´gy, hogy ugyanabban a sorban vagy oszlopban nem szerepelhet többször ugyanaz a szám. N -et a latin négyzet rendjének nevezz¨ uk, teh´ at péld´ aul a 3.1. ´ abrán szerepl˝o táblázat rendje 4. Az lsencode el˝oször egy teljesen kit¨ olt¨ ott négyzetet gener´ al, majd ebb˝ol kitöröl néhány elemet, ´ıgy lyukakat képezve. A feladat a szab´ alyok szerint kit¨ olteni ezeket, akárcsak az ismert sudoku játékban. Az ´ıgy generált problém´ aknak mindenképpen lesz legal´ abb egy megoldása: az a teljes táblázat, amit éppen mi generáltunk. Ahogy

21

Bart´ ok D´ avid


az 1.2-es fejezetben eml´ıtettem, nagyon sok matematikai probléma értelmezhet˝o SAT-ként, péld´ aul a latin négyzetek is. Az lsencode ennek megfelel˝oen a generált problémákat képes SAT-tá konvert´ alni. Nyilv´ anval´ o, hogy a probléma nehézsége a négyzet rendjének f¨ uggvényében szigor´ uan monoton n˝ o. A lyukak ar´ any´ anak a nehézséggel való kapcsolata azonban egészen másként alakul.

Probléma nehézsége

30%

35%

Lyukak aránya

3.2. ´ abra. A probléma nehézségének alakulása A 3.2. ´ abr´ an l´ athatjuk, hogy a probléma akkor a legnehezebb, hogyha a lyukak aránya a mez˝ okh¨ oz képest 30% és 35% k¨ oz¨ ott van. Ennek az az oka, hogy ha nagyon kevés a lyuk, akkor a megold´ as elég egyértelm˝ u, ha pedig nagyon sok az u ¨res hely, akkor sokféle jó kitöltés lehetséges. Viszonylag sz˝ uk az a ter¨ ulet, ahol az igaz´ an nehéz problémapéldányok helyezkednek el. A program haszn´ alata parancssori argumentumok seg´ıtségével történik a következ˝o m´ odon: el˝ osz¨ or gener´ alunk egy adott méret˝ u, kitöltött négyzetet, majd egy másik paranccsal lyukakat tesz¨ unk bele. Az lsencode pls formátumban tárolja a problémákat, azonban beép´ıtett konverterével atalak´ıthatjuk ezeket cnf f´ ´ ajlokk´ a. Az ´ altalam alkalmazott m´ asik generátor a ToughSat [18]. Ez egy online használható, vagy ak´ ar le is t¨ olthet˝ o program, ami rengeteg opcióval rendelkezik a generált példányok tulajdonságait illet˝ oen. T´ amogatja a m´ ar kor´ abbiakban eml´ıtett pr´ımtényez˝okre bontás problémák kész´ıtését is, amelyeket a teszteléskor én is el˝ oszeretettel használtam.

3.3.

BCAT

A BCAT (Budapest Complexity Analysis Toolkit) [6] egy algoritmusok tesztelésére C++-ban kifejlesztett szoftvercsomag. 4 f˝ o¨ osszetev˝ob˝ol áll: problémák (problems), algoritmusok (algorithms), elemz˝ ok (analyzers), és konverterek (converters). A probléma bármilyen jelleg˝ u lehet, támogatott a f´ ajlb˝ ol t¨ ortén˝ o beolvas´ as és a generelás is. Az algoritmusok lehetnek teljes egészében a BCAT-be implement´ alva mint f¨ uggvények, de akár egy k¨ uls˝o exe fájlként is megh´ıvhatók. A BCAT r¨ ogz´ıti az algoritmusok fut´ asi idejét, és az általuk talált megoldást is. Az elemz˝ok szintén problém´ akra haszn´ alhat´ oak, de nem megoldj´ ak azokat, hanem a problémák valamilyen tulajdonságáról gy˝ ujtenek inform´ aci´ ot. Ez az algoritmusok hatékonyságának vizsgálatánál hasznos lehet az összef¨ uggések kereséséhez. A konverterek egy problémát egy másik fajta problémává tudnak átalak´ıtani, péld´ aul ILP-t SAT-t´ a. Ez´ altal egy adott solvert többféle problémára is tudunk használni. A BCAT-nek egy konfigur´ aci´ os fájlon kereszt¨ ul mondhatjuk meg, hogy mely problémákra mely algoritmust, elemz˝ ot vagy konvertert futtassa. Ez egy, a C++-hoz nagyon hasonló, le´ıró nyelven

22

Bart´ ok D´ avid


t¨ orténik. Fontos, hogy a gener´ alt problémák és az algoritmusok paraméterezhet˝ok, és a BCAT a paraméterek ¨ osszes lehetséges kombinációjára, az összes problémára lefuttatja az algoritmust. A tesztelés eredményét a BCAT egy csv (comma-separated values) fájlban tárolja, amelyb˝ol péld´ aul Excel seg´ıtségével k¨ onnyedén kész´ıthet˝o grafikon. A BCAT sz´ amos beép´ıtett problémat´ıpust és algoritmust tartalmaz, de természetesen saj´ at algoritmusok tesztelésére is alkalmas. Ehhez nem kell mást tenn¨ unk, mint az UI (user interface) seg´ıtségével hozz´ aadni a k´ıv´ ant algoritmust. Az algoritmusunknak megfelel˝oen kell kezelnie a BCAT altal sz´ ´ am´ ara ´ atadott paramétereket (a konfigurációs fájlból), és meg kell oldanunk a BCAT-tel val´ o kommunik´ aci´ oj´ at is.

23

4. fejezet

Az algoritmus 4.1.

Logikai szint

Ebben a fejezetben ¨ osszefoglalom a best-first search seg´ıtségével gyors´ıtott SAT-solver m˝ uködését és el˝ onyeit.

4.1.1.

Az alap¨ otlet (. . . )

(1. solver)

(2. solver)

(1)

(. . . )

(2) (. . . ) ø

(4) (3) ø

(5) ø

(. . . ) ø

(. . . ) (. . . ) ø

(6)

(. . . ) ø

(. . . ) ø

(. . . )

(7)

(. . . ) (8) ø

(. . . ) ø

(. . . )

(9) X

(. . . ) ø

(. . . ) ø

(. . . ) (. . . ) ø

(. . . ) ø

(. . . ) (. . . ) ø

4.1. ábra. Best-first search 2 solverrel Az algoritmus a k¨ ovetkez˝ oképpen gyors´ıthatja fel a SAT-solver m˝ uködését: felbontjuk a keresési f´ at valah´ any részre, amelyek k¨ oz¨ ul mindegyikben egy k¨ ulön solver végzi a keresést. A 4.1. ´ abr´ an ezt 2 solverrel szemléltetem: az egyik elind´ıtja a keresést, majd két ellentmondásra is akad (3. és 5. cs´ ucs). Ezut´ an a 2. solver fog futni, majd a 9. lépésben megoldást is talál. Nagyobb problém´ ak esetén nyilv´ anval´ oan t¨ obbsz¨ or is válthatunk solvert. Vegy¨ uk észre, hogy a péld´ aban az els˝o solver részfájában egyáltalán nincsen megoldás. Akár az is lehetséges, hogy egy t¨ obb ezer v´ altozóból álló probléma esetén ugyanez fordul el˝o: az els˝o értékad´ as hat´ as´ ara egy olyan részf´ aba ker¨ ul¨ unk, ahol nincsen megoldás, de a fa másik felében akár t¨ obb is tal´ alhat´ o. Ebben az esetben a fa egyik felét teljesen feleslegesen járjuk be, miel˝ott átker¨ ul¨ unk a

24

(. . . ) X

Bart´ ok D´ avid


´ m´ asik részf´ ara. Eppen emiatt tal´ alták ki a restartokat: a hossz´ u eredménytelen keresés arra utal, hogy a solver egy ilyen részf´ an tartózkodik. Hogyha az u ´jraind´ıtás után az els˝o értékadás máshogy t¨ orténik, val´ osz´ın˝ uleg egy kedvez˝ obb részfára ker¨ ul¨ unk, ezáltal hamarabb találunk megoldást. Ugyanerre a problém´ ara ny´ ujt megoldást a best-first search is, azonban több el˝onye is van. Egyrészt a solverv´ alt´ as ut´ an nem vesznek el az addigi eredmények, tehát ha például szeretnénk visszatérni az 1. részf´ aba, akkor nem a legelejér˝ol kell elkezden¨ unk a keresést. Egy nagyobb probléma esetén, ahol sokszor oda-vissza v´ altogatunk a solverek között, ez sok id˝ot takar´ıthat meg. Másrészt ez az algoritmus a restarttal ellentétben garantálja azt, hogy kiker¨ ul¨ unk az eddig vizsgált részf´ ab´ ol, és teljesen m´ asik ter¨ uletet fogunk vizsgálni. Harmadrészt pedig, a solverekhez rendelt heurisztikus pontsz´ am miatt mindig azon a részen fogunk keresni, ahol a legnagyobb valósz´ın˝ uséggel tal´ alhat´ o megold´ as.

4.1.2.

A keres´ esi t´ er sz´ etoszt´ asa

A keresési tér szétoszt´ as´ ahoz el kell érn¨ unk azt, hogy mindegyik solver csak a neki kijelölt részf´ an végezze a keresést. Ahogy a 3.1-es fejezetben eml´ıtettem, ezt a MiniSat által biztos´ıtott assumption¨ ok seg´ıtségével oldjuk meg. Ha ez a funkció nem létezne, egy saját kész´ıtés˝ u f¨ uggvénnyel kellene vezéreln¨ unk az els˝ o néh´ any értékadást, hogy a solverek a megadott hely¨ ukre ker¨ uljenek a f´ aban. Ez esetben arra is kellene figyeln¨ unk, hogy a solver a backtrack során ne ugorjon ki a neki sz´ ant részf´ ab´ ol. Az assumption¨ ok k¨ onnyebbé teszik a fa részekre osztását, hiszen az eml´ıtett feladatokat elvégzik helyett¨ unk. (. . . )

(. . . )

(. . . )

1. solver x0 =0 x1 =0 x2 =0

2. solver x0 =0 x1 =0 x2 =1

(. . . )

(. . . )

(. . . )

3. solver x0 =0 x1 =1 x2 =0

4. solver x0 =0 x1 =1 x2 =1

5. solver x0 =1 x1 =0 x2 =0

6. solver x0 =1 x1 =0 x2 =1

(. . . )

7. solver x0 =1 x1 =1 x2 =0

8. solver x0 =1 x1 =1 x2 =1

4.2. ´ abra. 8 solver megvalós´ıtása assumptionökkel A 4.2. ´ abra 8 solverre mutatja be azt, hogy hogyan lehetséges a keresési tér szétosztása assumption¨ ok haszn´ alat´ aval: vessz¨ uk k v´ altozó összes interpretációját, ami a 2.3.1-es fejezetnek megfelel˝ oen éppen 2k . Ezeket az interpret´ aci´ okat elképzelhetj¨ uk u ´gy is, hogy k döntés után ennyi féle k¨ ulönb¨ oz˝ o cs´ ucson lehet¨ unk éppen a f´ aban. Ha ezen cs´ ucsok mindegyike egy solver számára jelenti a kiindul´ asi pontot a keresésben, akkor siker¨ ult a keresési teret 2k részre osztanunk. Látható, hogy ha ezt a m´ odszert haszn´ aljuk, akkor a használt solverek száma (numSolvers) 2 hatványa kell, hogy legyen. Megoldhat´ o lenne tetsz˝ oleges szám´ u solver használata is, azonban ez azt jelentené, hogy a solverek k¨ ul¨ onb¨ oz˝ o d¨ ontési szintekr˝ol indulnak a keresésben (egy adott döntési szinten mindig 2k cs´ ucs tal´ alhat´ o). Ez nem feltétlen¨ ul jelentene problémát, azonban a heurisztikát sz¨ ukségtelen¨ ul bonyolultt´ a tenné. A keresési fa feldarabol´ as´ an´ al a solverek száma egyértelm˝ uen meghatározza, hogy hány változ´ ot adunk az egyes solvereknek assumptionként. Arról azonban, hogy ezek mely változók legyenek, 25

Bart´ ok D´ avid


szabadon d¨ onthet¨ unk. Ez azt jelenti, hogy azt, hogy mi alapján osztjuk szét a keresési teret, mi d¨ ontj¨ uk el ezen v´ altoz´ ok kiv´ alasztásával. Felmer¨ ul a kérdés, hogy mely változókat célszer˝ u erre a célra haszn´ alni. A legegyszer˝ ubb az, hogy 2k solver esetén ezek legyenek x0 , x1 , . . . , xk−1 . Egy m´ asik lehet˝ oség, hogy a legt¨ obb kl´ ozban el˝oforduló változókat használjuk. Ez azért lehet jó ötlet, mert ´ıgy val´ osz´ın˝ uleg egym´ ast´ ol nagyon k¨ ulönböz˝o kiindulási alapot kapnak a solverpéldányok, és ´ıgy tal´ an pontosabban meg tudjuk hat´ arozni, hogy melyiket is érdemes futtatni. Arra, hogy ez valóban ´ıgy van-e, a Mérések fejezetben fogunk választ kapni.

4.1.3.

A heurisztika

A best-first searchben fontos elem a solverek sikerességét kiértékel˝o heurisztikus f¨ uggvény. Ebben a fejezetben azt ismertetem, hogy milyen adatokat célszer˝ u használni ebben a f¨ uggvényben. Ehhez azt kell végiggondolnunk, hogy mi jelzi el˝ore azt, ha egy SAT-solver közel jár a megoldáshoz. Azt is figyelembe kell venn¨ unk, hogy ezen tényez˝ok köz¨ ul némelyikhez esetleg olyan mérték˝ u adatgy˝ ujtés is sz¨ ukséges lehet, hogy a jelentkez˝o overhead miatt azok alkalmazása nem éri meg. • Jelenleg h´ any v´ altoz´ onak van értéke? Minél több változó rendelkezik már valamilyen értékkel, ann´ al val´ osz´ın˝ ubb, hogy néhány további döntés után megoldásra jutunk. • Mennyi az eddig elért maximális mélység? Ha egy solver már nagyon mélyen is járt a keresési f´ aban, val´ osz´ın˝ us´ıthet˝ o, hogy hamar megoldást ad. • Mennyi az ´ atlagos mélység? A sikerességet szintén jelezheti az, hogy a solver átlagos mélysége a keresés sor´ an nagy. • Milyen hossz´ uak a tanult klózok? A rövid tanult klózok jobban használhatóak, hiszen egy er˝ osebb feltételt fogalmaznak meg, ezzel lesz˝ uk´ıtve a keresést. Leghasznosabbak az egy liter´ alb´ ol ´ all´ ok, hiszen egy ilyen az adott változó értékét egyértelm˝ uen meghatározza. Ezen ¨ otletek alapj´ an a kiértékel˝o f¨ uggvény a következ˝oképpen ép¨ ul fel: score = f (currentDepth, maxDepth, averageDepth, averageLearntClauseLength) Természetesen ez ebben a formában csak egy ötlet, aminek a helyességét a mérések során kell ellen˝ orizn¨ unk. Lehetséges, hogy a fenti feltételezések köz¨ ul némelyik nem jelzi el˝ore a megold´ as k¨ ozelségét, és azt is meg kell vizsg´ alnunk, nem sz¨ ukséges-e ezek valamelyikéhez t´ ul sok adatgy˝ ujtés. A CDCL le´ır´ as´ ar´ ol sz´ ol´ o fejezetben eml´ıtettem, hogy a futás során nem minden adatot tudunk az egyes kl´ ozokr´ ol kinyerni a speciális adatszerkezet miatt. Ez azt jelenti, hogy nem tudjuk péld´ aul meg´ allap´ıtani, hogy egy kl´ ozon bel¨ ul hány változónak van értéke. Ezt tehát nem tudjuk alkalmazni a heurisztik´ aban.

4.2.

Implement´ aci´ o

A BFS algoritmus MiniSatba val´ o implementálása során a következ˝o elveket követtem: • A m´ odos´ıt´ asokat pr´ ob´ altam a main() f¨ uggvényre korlátozni, azaz a solver lényegi m˝ uködésében nem akartam jelent˝ os m´ odos´ıtásokat létrehozni. • A MiniSat alapb´ ol meglev˝ o funkcióit semmilyen módon nem szerettem volna korlátozni, csup´ an a problém´ ak megold´ asi folyamatát gyors´ıtani. • A v´ altoztat´ asokat u ´gy eszk¨ ozöltem, hogy azok a MiniSat többi részével azonos adatszerkezeteket haszn´ aljanak.

26

Bart´ ok D´ avid

4.2.1.


Az eredeti MiniSat m˝ uk¨ od´ ese

Ebben a fejezetben r¨ oviden ismertetem a MiniSat m˝ uködését, hiszen ezen ismeretek fontosak ahhoz, hogy megérts¨ uk, miben k¨ ul¨ onb¨ ozik az eredeti MiniSattól a best-first search. A MiniSat ´ altal haszn´ alt adatt´ıpusok a következ˝ok: vec: Template-es´ıtett, t¨ omb¨ ot megvalós´ıtó osztály. Lit: Liter´ alokat t´ arol. CRef: Kl´ ozokat t´ arol. A MiniSat main() f¨ uggvényének részletes m˝ uködése: El˝ osz¨ or be´ all´ıt´ asra ker¨ ulnek az argumentumokban kapott opciók, majd, ha a bemeneti fájl elérési u ´tvonala megfelel˝ o, a MiniSat beolvassa egy Solver t´ıpus´ u objektumba a cnf fájlból a klózokat. Ezut´ an h´ıv´ odik meg a simplify() f¨ uggvény, amely még a keresés el˝ott elvégez egy unit propagationt. Ha a solver ezalatt ellentmond´ asra jut, a probléma unsatisfiable. Egyéb esetben elkezd˝ odik a probléma megoldása. Ez a solveLimited() f¨ uggvény seg´ıtségével t¨ orténik, amelynek bemen˝ o paramétere a keresésnél figyelembe veend˝o assumptionök listája. Ha nem szeretnénk assumption¨ oket haszn´ alni, egy u ¨res tömböt kell beadnunk a f¨ uggvény paramétereként. A solveLimited() f¨ uggvény csupán annyit csinál, hogy átmásolja a paraméterében kapott asuggvényt. A sumption t¨ omb¨ ot a Solver assumptions nev˝ u változójába, ezután megh´ıvja a solve () f¨ fentiekb˝ ol k¨ ovetkezik, hogy a solve () megh´ıvásának el˝okövetelménye, hogy az assumptions bels˝ o v´ altoz´ o m´ ar inicializ´ alva legyen. A solve () f¨ uggvény tulajdonképpen egy while ciklusban futtatja a search() f¨ uggvényt, ami a tényleges keresést végzi. Erre azért van sz¨ ukség, mert a search() f¨ uggvény paraméterként egy egész sz´ amot kap, és ennyi darab konfliktus után visszatér, de megoldás nélk¨ ul (l Undef). Egészen addig maradunk a while cikluson bel¨ ul, am´ıg a search() f¨ uggvény vagy l Unsat (unsatisfiable) vagy l Sat (satisfiable) értékkel nem tér vissza. Minden egyes, eredményre nem jutó keresés után növelésre ker¨ ul a limitként adott konfliktusok száma, és u ´jra megh´ıvódik a search(). 1 2 3 4 5

inline lbool Solver::solveLimited (const vec& assumps) { assumps.copyTo(assumptions); return solve (); }

6 7 8 9 10 11 12 13 14 15 16 17 18

lbool Solver::solve () { ... while (status == l Undef) { ... status=search(rest base∗restart first); ... } ... return status; } L´ athatjuk, hogy a seach() f¨ uggvény a megengedett konfliktusok számát egy szorzat formáj´ aban kapja. Ezek k¨ oz¨ ul a restart first egy konstans, a rest base minden visszatérés után n˝o, ´ıgy biztos´ıtva azt, hogy a f¨ uggvény egyre nagyobb limittel rendelkezzen. Az alapbeáll´ıtás szerint a rest base exponenci´ alisan n¨ ovekszik, de ezt a felhasználó módos´ıthatja. A keresés befejezése után történik a megold´ as output f´ ajlba ´ır´ asa, a lefoglalt memóriater¨ ulet felszabad´ıtása, majd a kilépés.

27

Bart´ ok D´ avid

4.2.2.


Inicializ´ al´ as

A BFS implement´ aci´ oj´ ahoz az els˝ o lépés az, hogy több solver legyen jelen egyszerre, és ezek mindegyikének legyen egy pontsz´ ama, ami alapján meg tudjuk mondani, mennyire állnak közel a probléma megold´ as´ ahoz. Ezt a k¨ ovetkez˝ o strukt´ ura seg´ıtségével valós´ıtottam meg: 1 2 3 4 5

struct BestFirst { Solver∗ Slv; double score; }; A BestFirst strukt´ ura elemei tehát: egy Solver t´ıpus´ u pointer, és a solverhez tartozó aktu´ alis pontsz´ am. A programban haszn´ alt solvereket egy BestFirst t´ıpus´ u pointerekb˝ol álló vektorban t´ arolom:

1

vec S; A SAT-probléma f´ ajlb´ ol t¨ ortén˝ o beolvasása egy for ciklusban történik, méghozzá annyiszor, ah´ any solvert szeretnénk haszn´ alni. Ezen természetesen lehetne gyors´ıtani: a Solver objektumhoz ajánlatos kész´ıteni egy m´ asol´ o konstruktort. A kutatásom során ett˝ol eltekintettem, mert a méréseim azt mutatt´ ak, hogy a probléma beolvas´ asa nagyságrendekkel kevesebb id˝ot vesz igénybe, mint a megold´ as tényleges keresése.

1 2 3 4 5 6 7 8

for(int ii=0; iiscore=INFINITE; //initialise score S[ii]−>Slv=new Solver; ... } Maga a beolvas´ as teljesen analóg az eredeti MiniSat megoldásaival, annyi a k¨ ulönbség, hogy az S[ii] strukt´ ura Slv tagv´ altoz´ oj´ aba kell betölten¨ unk az adatokat. Az INFINITE egy predefiniált konstans, értéke a score v´ altoz´ oban t´ arolható legnagyobb érték kell, hogy legyen. A solverek pontsz´ am´ at azért erre az értékre inicializ´ aljuk, hogy a következ˝o solver kiválasztásnál preferálva legyenek a még nem haszn´ alt solverek azokkal szemben, amelyek már a heurisztika alapján pontszámmal rendelkeznek. Ennek megfelel˝ oen csak akkor választunk solvert a heurisztika alapján, ha már mindegyikr˝ ol rendelkez¨ unk val´ odi adatokkal (amiket a futás során gy˝ ujtött¨ unk). Annak kiv´ alaszt´ as´ ar´ ol, hogy mely változókat adjuk meg assumptiönként, a kés˝obbiekben lesz sz´ o. Egyel˝ ore tegy¨ uk fel, hogy egy occurdata nev˝ u strukt´ uratömb els˝o log2 numSolvers helyén all´ ´ o v´ altoz´ ok adj´ ak meg az assumptionöket, az index nev˝ u tagváltozójukban, a következ˝oképpen: occurdata[0].index, occurdata[1].index stb. Az assumptionök létrehozását a következ˝o kódrészlet szemlélteti:

28

Bart´ ok D´ avid


0 = 000 ⇒ x0 ∧ x1 ∧ x2 1 = 001 ⇒ x0 ∧ x1 ∧ ¬x2 2 = 010 ⇒ x0 ∧ ¬x1 ∧ x2 3 = 011 ⇒ x0 ∧ ¬x1 ∧ ¬x2 4 = 100 ⇒ ¬x0 ∧ x1 ∧ x2 5 = 101 ⇒ ¬x0 ∧ x1 ∧ ¬x2 6 = 110 ⇒ ¬x0 ∧ ¬x1 ∧ x2 7 = 111 ⇒ ¬x0 ∧ ¬x1 ∧ ¬x2 4.3. ´ abra. A solver száma és a hozzá tartozó assumption-tömb

1 2 3 4 5 6 7 8 9 10 11 12 13 14

int binary; Lit L; int cntr; for(int ii=0; ii1; jj/=2) //assumption list for a solver { L=mkLit(occurdata[cntr++].index, binary%2); //making of a literal S[ii]−>Slv−>assumptions.push(L); //add the literal binary/=2; //next position } } A k´ odrészlet némi magyar´ azatot igényel. Képzelj¨ uk el, hogy numSolvers darab solvert szeretnénk futtatni a keresési f´ an. Tudjuk, hogy az assumptionök száma log2 numSolvers, és hogy mindegyiknek k¨ ul¨ onb¨ oz˝ onek kell lennie. Az assumptionök tulajdonképpen log2 numSolvers hossz´ u bitsorozatok, amelyek megadják az egyes változók polaritását. Ezekb˝ol következik, hogy a solver sorsz´ ama egyértelm˝ uen hozzárendel egy adott assumption-tömböt, hogyha a sorsz´ amot log2 numSolvers jegy˝ u, kettes sz´ amrendszerbeli számként tekintj¨ uk. Ez látható a 4.3. ábrán. A k¨ uls˝ o for ciklusban a solvereken iterálunk végig. Minden iteráció elején inicializáljuk a cntr v´ altoz´ ot, ami azt mutatja meg, hogy hanyadik assumptiont adjuk be az adott solvernek; tovább´ aa binary v´ altoz´ oban t´ arolt assumption-kódot. A bels˝o ciklusban történik maga az assumptions t¨ omb felép´ıtése. Ezzel a viszonylag egyszer˝ u, rövid kódrészlettel történik tehát a keresési fa szétoszt´ asa.

4.2.3.

Az assumption¨ okben szerepl˝ o v´ altoz´ ok meghat´ aroz´ asa

Ebben a fejezetben r¨ oviden ismertetem, hogyan lehet egy cnf fájlból kinyerni azt, hogy melyik v´ altoz´ o h´ anyszor szerepel benne. Erre a 4.1.2-es fejezetben eml´ıtettek miatt van sz¨ ukség: meg szeretnénk vizsg´ alni, hogy érdemes-e a leggyakrabban el˝oforduló változókat használni az assumptionökben. A MiniSat cnf f´ ajlb´ ol t¨ ortén˝ o beolvasási folyamatát u ´gy módos´ıtottam, hogy elmentse azt, hogy az egyes v´ altoz´ ok h´ anyszor szerepelnek a kifejezésben összesen. A kódban a sz¨ urkével kiemelt részek az én m´ odos´ıt´ asaim ennek a mérésére. A megval´ os´ıt´ asra a k¨ ovetkez˝ o strukt´ ura szolgált:

29

Bart´ ok D´ avid

1 2 3 4 5


struct var occur { int count; //how many times the variable occured int index; //index of the variable };

6 7

1 2 3 4 5 6 7 8

var occur∗ occurdata; parse DIMACS main(InputStream in, Solver S) { vec lits; while(in != EOF) { if(in == ’p’) { vars=parseInt(in); occurdata=new var occur[vars]; for(int ii=0; ii
9 10 11 12

occurdata[ii].count=0;

13

occurdata[ii].index=ii; } clauses=parseInt(in);

14 15

} else if (in == ’c’ || in == ’p’) skipLine(in); else { readClause(in, S, lits); S.addClause (lits); }

16 17 18 19 20 21 22 23

}

24 25

}

26 27 28 29 30 31 32 33

static void readClause(InputStream in, Solver S, vec lits) { while (true) { parsed lit=parseInt(in); if (parsed lit == 0) break; increaseCount(occurdata, var); addLiteral(lits, parsed lit);

34 35

}

36 37

} • parseInt(): Beolvas egy egész számot egy fájlból. ´ • skipLine(): Atugorja a kommentként szolgáló sort. 30

Bart´ ok D´ avid


• addClause(): Hozz´ aad egy literáltömböt a már meglev˝o klózok listájához. • addLiteral(): Hozz´ aad egy literált a paraméterként kapott literáltömbhöz. oveli eggyel az adott változó el˝ofordulásának számát a nyilvántart´ asra • increaseCount(): megn¨ szolg´ al´ o t¨ ombben Miut´ an rendelkezés¨ unkre ´ allnak a sz¨ ukséges adatok, az occurdata tömböt egyszer˝ uen count szerint n¨ ovekv˝ o sorrendbe kell rendezn¨ unk, a tömb elején ´ıgy a leggyakoribb változók lesznek (az index tagv´ altoz´ okban).

4.2.4.

A keres´ es

A solverek és assumption¨ ok inicializálása után megkezd˝odhet maga a best-first search. Ez egy ciklusban fut, ahol minden iter´ aci´ o elején növelj¨ uk az adott solverpéldánynak adott konfliktuslimitet. Ezut´ an a megadott sz´ am´ u konfliktus eléréséig keres¨ unk az aktuális solverrel, és a visszatérési értéknek megfelel˝ oen halad tov´ abb a program. Ez az érték háromféle lehet: SAT: a solver egy megold´ ast tal´ alt UNSAT: a solver befejezte a keresést, a hozzá rendelt részfában nincs megoldás UNRESOLVED: a solver részf´ aj´ aban lehet megoldás, de még nem találtuk meg azt Ha egy solver SAT-tal tér vissza, akkor kiléphet¨ unk a ciklusból, a probléma satisfiable. UNSAT érték esetében két eset lehetséges, attól f¨ ugg˝oen, hogy van-e még m˝ uköd˝oképes solver. Amennyiben nincs, akkor a probléma unsatisfiable. Ha van még akt´ıv solver, akkor kiválasztjuk, hogy melyik folytatja a keresést. Ha pedig UNRESOLVED a visszatérési érték, akkor a feladatunk pontsz´ amot rendelni az aktu´ alis solverhez és kiválasztani a következ˝oként futtatásra ker¨ ul˝o példányt. A MiniSatba implement´ alt best-first search algoritmus pszeudokódja ennek megfelel˝oen a következ˝oképpen alakul:

31

Bart´ ok D´ avid

1 2 3 4 5 6


BFS(SolverList L) { Solver currentSolver; boolean satisfied=false; // true, if a solver has returned SAT boolean exists active solver=true; // true, if we have an active solver while(NOT(satisfied) AND exists active solver)

7

currentSolver=findMaxHeuristic(L); limit=increaseLimit();

8 9 10

retCurr=solve(currentSolver, limit);

11 12

if(retCurr == UNRESOLVED) setHeuristic(currentSolver);

13 14 15

else if(retCurr == SAT) gatherStats(currentSolver); satisfied=true;

16 17 18 19

else if(retCurr == UNSAT) gatherStats(currentSolver); deAllocate(currentSolver); exists active solver=activeCheck(L);

20 21 22 23 24

printStats(); if(satisfied) return true; if(NOT(exists active solver)) return false;

25 26 27 28 29 30

} • Solver currentSolver: Az éppen futtatott solver. • increaseLimit(): Minden futtatás el˝ott megnöveli a solvernek adott konfliktuslimitet. • solve(): Keres a f´ aban, visszatér ha eredményre (SAT vagy UNSAT) jutott, illetve ha eléri a paraméterben megadott konfliktusszámot (UNRESOLVED). • setHeuristic(): Egy pontsz´ amot rendel a solverhez, a futási adatok alapján • findMaxHeuristic(): Egy egyszer˝ u maximumkereséssel (pontszám alapján) kiválaszatja a k¨ ovetkez˝ oként futtat´ asra ker¨ ul˝o solvert. • gatherStats(): Elmenti a solver adatait a futás befejezése utáni statisztika kész´ıtéséhez. • deAllocate(): Felszabad´ıtja a solver által használt memóriater¨ uletet. • activeCheck(): Igaz értéket ad vissza, ha van még m˝ uköd˝o solver¨ unk. • printStats(): A fut´ as végén ki´ırja a solverekkel kapcsolatos statisztikai adatokat.

32

5. fejezet

M´ er´ esek MiniSat without restarts MiniSat with restarts numSolvers:8,heuristic:3,limit:1000,increase:150,assump_vars:1 numSolvers:8,heuristic:3,limit:1000,increase:150,assump_vars:0 numSolvers:8,heuristic:3,limit:1000,increase:110,assump_vars:1 numSolvers:8,heuristic:3,limit:1000,increase:110,assump_vars:0 numSolvers:8,heuristic:2,limit:1000,increase:150,assump_vars:1 numSolvers:8,heuristic:2,limit:1000,increase:150,assump_vars:0 numSolvers:8,heuristic:2,limit:1000,increase:110,assump_vars:1 numSolvers:8,heuristic:2,limit:1000,increase:110,assump_vars:0

numSolvers:8,heuristic:1,limit:1000,increase:150,assump_vars:1 numSolvers:8,heuristic:1,limit:1000,increase:150,assump_vars:0 numSolvers:8,heuristic:1,limit:1000,increase:110,assump_vars:1

numSolvers:8,heuristic:1,limit:1000,increase:110,assump_vars:0 0

2

4

6

8

10

12

14

16

Futásidő (s)

5.1. ´ abra. A best-first search változatok eredményei Az els˝ o grafikonon (5.1. ´ abra) 14 k¨ ulönböz˝o solver változat futási idejének összehasonl´ıt´ asa l´ athat´ o. A solverek k¨ oz¨ ott szerepel az eredeti MiniSat restarttal és anélk¨ ul, valamint 12 best-first search v´ altozat is. Mindegyik solvert ugyanazon a 20 problémán futtattam, és a futásid˝ok átlag´ at abr´ ´ azoltam a grafikonon. A tesztelésre használt problémapéldányokat az lsencode seg´ıtségével gener´ altam, ebb˝ ol k¨ ovetkezik, hogy ezek mind megoldhatóak. A példányok mindegyike egy 35 × 35 méret˝ u, 44% lyukat tartalmaz´ o véletlenszer˝ u latin négyzet SAT-problémaként való megfogalmaz´ asa. Az lsencode-r´ ol sz´ ol´ o fejezetben l´ athattuk, hogy a lyukak száma drasztikusan befolyásolja a probléma nehézségét. Ennek megfelel˝ oen én viszonylag nagy lyukarányt használok, és a nehézséget ink´ abb a t´ ablamérettel szab´ alyozom. A generált cnf fájlok kb. 4 000 változót és 40 000 klózt tartalmaznak. Az el˝ ozetes vizsg´ alatok sor´ an számos heurisztikát kipróbáltam, ezek köz¨ ul csak a 3 legsikeresebb vett részt a végs˝ o tesztelésekben. A best-first search¨ ot alkalmaz´ o solverek paraméterei a következ˝ok: • numSolvers: a solverpéld´ anyok száma • heuristic: a heurisztika kisz´ am´ıtásának módja 1: score = averageDepth/averageLearntClauseLength 2: score = currentDepth + maxDepth 3: score = currentDepth ∗ averageDepth/averageLearntClauseLength 33

Bart´ ok D´ avid


• limit: a solverek el˝ osz¨ or h´ any konfliktusig futnak • increase: a limitet mindig ilyen mértékben változtatjuk százalékban értve, pl.: 110 esetén mindig 1,1-szeres lesz a n¨ ovekedés • assump vars: mely v´ altoz´ ok szerint kapják a solverek az assumptionöket 0: els˝ o k v´ altoz´ o 1: leggyakoribb v´ altoz´ ok Ez a teszt t¨ obb szempontb´ ol is rendk´ıv¨ ul tanulságos. A best-first search összes változata gyorsabb, mint a restart nélk¨ uli MiniSat, de az u ´jraind´ıtásokat használó változatot nem igazán siker¨ ult fel¨ ulm´ ulni. Nyilv´ anval´ o lett az is, hogy a leggyakrabban szerepl˝o változókat célszer˝ u az assumption¨ okben haszn´ alni, és hogy a 3-as heurisztika nem megfelel˝o. L´ athatjuk teh´ at, hogy a best-first searchöt valahogyan kombinálni kellene az eredeti MiniSat u ´jraind´ıt´ asaival. A tov´ abbi tesztekben a best-first search egy átalak´ıtott változatát haszn´ alom, ahol a heurisztika kisz´ am´ıt´ asa ut´ an mindig u ´jraind´ıtom az adott solvert. Így valósz´ın˝ uleg mindig a leg´ıgéretesebb solvert fogjuk futtatni, azonban a restartokat is alkalmazzuk az algoritmus tov´ abbi gyors´ıt´ as´ ara.

MiniSat without restarts MiniSat with restarts numSolvers:16,heuristic:2,limit:100,increase:150,assump_vars:1

numSolvers:16,heuristic:2,limit:100,increase:110,assump_vars:1 numSolvers:16,heuristic:1,limit:100,increase:150,assump_vars:1 numSolvers:16,heuristic:1,limit:100,increase:110,assump_vars:1 numSolvers:8,heuristic:2,limit:100,increase:150,assump_vars:1 numSolvers:8,heuristic:2,limit:100,increase:110,assump_vars:1 numSolvers:8,heuristic:1,limit:100,increase:150,assump_vars:1 numSolvers:8,heuristic:1,limit:100,increase:110,assump_vars:1 numSolvers:4,heuristic:2,limit:100,increase:150,assump_vars:1 numSolvers:4,heuristic:2,limit:100,increase:110,assump_vars:1 numSolvers:4,heuristic:1,limit:100,increase:150,assump_vars:1 numSolvers:4,heuristic:1,limit:100,increase:110,assump_vars:1

0

1

2

3

4

5

6

7

8

9

10

Futásidő (s)

5.2. ´ abra. Az u ´jraind´ıtásokkal gyors´ıtott BFS A m´ asodik grafikon (5.2. ´ abra) az el˝oz˝ovel azonos kör¨ ulmények között hasonl´ıtja össze a m´ odos´ıtott best-first search¨ ot az eredeti MiniSattal. Itt az el˝oz˝oekben legsikeresebb 1. és 2. heurisztik´ akat haszn´ alom, valamint csak a leggyakoribb változókat adom assumptionként. A tesztben azonban az el˝ oz˝ ot˝ ol eltér˝ oen t¨ obbféle solverszámot is kipróbálok. Itt m´ ar a restartot alkalmazó MiniSat is alulmarad a legtöbb BFS változattal szemben, k¨ osz¨ onhet˝ oen annak, hogy azokba is beleép´ıtettem az u ´jraind´ıtást. A harmadik grafikon (5.3. ´ abra) a legsikeresebb best-first search konfiguráció teljes´ıtményét mutatja be 100 k¨ ul¨ onb¨ oz˝ o problém´ an. Ennek paraméterei: • numSolvers=4 • heuristic=2 (score = currentDepth + maxDepth) • limit=100 34

Bart´ ok D´ avid


45

Előfordulások száma (db)

40 35 30 25

BFS

20

MiniSat 15 10 5 0

0-3

4-15

16-63

64-255

Futásidő (s)

5.3. ´ abra. A BFS és a MiniSat szórásának összehasonl´ıtása • increase=110 • assump vars=1 A tesztelésre haszn´ alt problémapéldányok immár nehezebbek: 39 × 39 méret˝ u latin négyzetek, 44% lyukkal, szintén lsencode ´ altal generálva. A generált cnf fájlok ´ıgy nagyjából 5 000 változ´ ot és 60 000 kl´ ozt tartalmaznak. Ez a grafikon más felép´ıtés˝ u, mint az el˝oz˝oek; azt mutatja be, hogy melyik solver h´ anyszor ny´ ujtott egy adott id˝ointervallumon bel¨ uli futásid˝ot. A jobb összehasonl´ıthat´ os´ ag érdekében a v´ızszintes tengelyen logaritmikus skálát használok, ez azt jelenti, hogy az orig´ ot´ ol t´ avolodva az ´ abr´ azolt intervallumok nagysága exponenciálisan n˝o. Az ábrán jól látható, hogy a best-first search fut´ asi ideje lényegesen jobb az eredeti MiniSat restartokat használó változat´ an´ al. A BFS 39-szer futott 16 m´ asodpercen bel¨ ul, m´ıg az eredeti MiniSat csupán 27-szer. A grafikonr´ ol ugyan nem olvashat´ o le, de meggy˝ oz˝o adat az átlagos futásid˝o is: a BFS esetében ez 46, 6 másodperc, m´ıg a MiniSatn´ al 59, 9. A negyedik grafikonon (5.4. ábra) egy u ´jabb, 30 problémán történ˝o tesztelés eredményeit l´ athatjuk. Itt m´ ar nem lsencode által generált példányokat használtam, hanem nagy sz´ amok pr´ımtényez˝ okre bont´ as´ anak SAT-problémává konvertált formáját. A felbontandó számok mindegyike két, 1 400 000 k¨ or¨ uli pr´ımszám szorzataként állt el˝o. Ennek az az oka, hogy az ´ıgy gener´ alt problém´ ak nehézsége a tesztekhez éppen megfelel˝o. Ezek a cnf fájlok kb. 1 500 változót és 7 500 kl´ ozt tartalmaznak. A haszn´ alt BFS algoritmus teljesen megegyezik az el˝oz˝o tesztben szerepl˝ ovel. Ezen az ´ abr´ an még jobban l´ atszik, hogy a BFS seg´ıtségével jelent˝osen csökkenthet˝o a szór´ as. Az eredeti MiniSatn´ al 8-szor ny´ ult 64 másodperc fölé a futásid˝o, m´ıg a BFS-nél ez csak 3-szor fordult el˝ o. A best-first search 30 futtat´ asból 23-szor 4 és 63 másodperc között végzett. Az átlagos fut´ asid˝ ok ennél a tesztnél a k¨ ovetkez˝ oképpen alakultak: a MiniSat esetében 43, 3 másodperc, a BFS-nél pedig 24, 9. A pr´ımtényez˝ ore bont´ as és az lsencode által generált problémák egymástól teljesen k¨ ulönb¨ oz˝ oek, mégis ugyanaz a BFS konfigur´ ació mindkét esetben nagyon jó eredményt ad. A módszer ilyen szempontb´ ol teh´ at elég robusztusnak tekinthet˝o.

35

Bart´ ok D´ avid


16

Előfordulások száma (db)

14

12 10

8

BFS MiniSat

6 4

2 0

0-3

4-15

16-63

64-255

Futásidő (s)

5.4. ´ abra. Sz´ or´ asok alakulása pr´ımtényez˝ore bontás-problémákon

36

6. fejezet

Befejez´ es 6.1.

Eredm´ enyek

A TDK-dolgozatomban bemutattam a best-first search algoritmus alkalmazását SAT-problém´ akra. Ehhez el˝ osz¨ or sz¨ ukséges volt a témához kapcsolódó elméleti háttér kör¨ uljárására. Az alapfogalmak ismertetése ut´ an kitértem mind az általános, mind a SAT-problémához használt speciális keres˝ o algoritmusok (DPLL és CDCL) felép´ıtésére is. Ezután következett a használt programok bemutat´ asa: a MiniSat az implement´ acióhoz volt elengedhetetlen; az lsencode, a ToughSat és a BCAT pedig a tesztelésben seg´ıtett. A kutatómunka le´ırása két szinten történt: egy absztrakt, logikai szinten, és a gyakorlati szinten. Ezen fejezet els˝o részében kitalált ötleteket tehát a második részben implement´ altuk a MiniSatba. Az ¨ otletek sokaságából ki kellett azonban választani, hogy mik azok, amelyek val´ oban gyors´ıtj´ ak az algoritmus m˝ uködését. Ennek menetét a mérésekr˝ol szóló fejezetben ismertettem, valamint a BFS hatékonyságát grafikonokkal támasztottam alá. Az adatgy˝ ujtés nagy sz´ am´ u futtatt´ as sor´ an, k¨ ul¨ onb¨ oz˝ o t´ıpus´ u és nehézség˝ u példányokon való teszteléssel történt, ´ıgy val´ os képet adva a hatékonys´ agr´ ol. A dolgozatb´ ol kider¨ ult, hogy a MiniSat tényleg könnyen módos´ıtható, akár az alapfelép´ıtését˝ ol lényegesen eltér˝ o algoritmusok megvalós´ıtására is képes. Ennek az oka, hogy objektumorient´ altan, egym´ ast´ ol j´ ol elk¨ ul¨ on¨ ul˝ o részek seg´ıtségével dolgozik. Fény der¨ ult továbbá arra is, hogy b´ ar a MiniSat egy nagyon hatékony solver, best-first search alkalmazásával a m˝ uködése tovább gyors´ıthat´ o, méghozz´ a jelent˝ os mértékben. Ehhez többféle paraméter kipróbálására volt sz¨ ukség, a legnagyobb att¨ ´ orést azonban az hozta, hogy a best-first searchöt kombináltuk a restarttal: ennek hatás´ ara az atlagos fut´ ´ asid˝ o mintegy 36%-kal csökkent. Ezt az ötletet a tesztek során a MiniSat u ´jraind´ıt´ asokat haszn´ al´ o v´ altozat´ anak eredményessége adta. A siker oka valósz´ın˝ uleg abban is keresend˝o, hogy a MiniSat eredetileg is gyakori u ´jraind´ıtásokra lett tervezve, és mivel az u ´jraind´ıtás során megtartjuk a tanult kl´ ozok egy részét, a keresés részeredményei sem vesznek teljesen el.

6.2.

Egy´ eb o ¨tletek

Az ´ altalam vizsg´ alt téma annyira szerteágazó, hogy a munkám során nem volt id˝om és lehet˝oségem ´ minden egyes felmer¨ ult ¨ otletet kipróbálni. Erdekes kérdés lehet az, hogy a problémák t´ıpus´ anak és méretének f¨ uggvényében hogyan célszer˝ u megadni a best-first search paramétereit. Lehet, hogy péld´ aul nagyobb méret˝ u problém´ ak esetén érdemes a limit növekedését máshogyan beáll´ıtani. Egy m´ asik lehetséges ir´ any az algoritmus fejlesztésére a tanult klózok közössé tétele. Ez a MiniSatban éppen a szigor´ uan elk¨ ul¨ on¨ ul˝o solver objektumok miatt nehézkes. Lehetséges azonban, hogy ez a funkci´ o nagyban gyors´ıtan´ a a BFS m˝ uködését. Szerencsés esetben egy 1 literálból álló tanult kl´ oz ak´ ar a haszn´ alt solverek felének munkáját feleslegessé tenné, ha ez a literál éppen szerepelt az

37

Bart´ ok D´ avid


assumption¨ okben. Az el˝ obbieken k´ıv¨ ul érdemes lehet még megvizsgálni az elért eredmények hardverf¨ uggését is. Lehet, hogy az u ´jraind´ıt´ as és a best-first search kombinációja azért sikeres, mert a solverváltáskor a cache tartalm´ at egyébként is ki kell u ¨r´ıten¨ unk. Emiatt, ha ezzel egyid˝oben egy restartot is elvégz¨ unk, nem n¨ ovelj¨ uk jelent˝ osen az overheadet. Az itt felmer¨ ult kérdésekkel a jöv˝oben behatóbban is k´ıvánok foglalkozni, remélhet˝oleg a BFS tov´ abbi gyors´ıt´ as´ at elérve.

38

Irodalomjegyz´ ek [1] Dimitris Achlioptas, Carla P. Gomes, Henry A. Kautz, and Bart Selman. Generating satisfiable problem instances. In Henry A. Kautz and Bruce W. Porter, editors, AAAI/IAAI, pages 256– 261. AAAI Press / The MIT Press, 2000. [2] Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P. Kurshan, and Kenneth L. McMillan. An analysis of SAT-based model checking techniques in an industrial environment. In Dominique Borrione and Wolfgang Paul, editors, Correct Hardware Design and Verification Methods, volume 3725 of Lecture Notes in Computer Science, pages 254–268. Springer Berlin Heidelberg, 2005. [3] Gilles Audemard and Lakhdar Sais. Circuit based encoding of CNF formula. In João MarquesSilva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing – SAT 2007, volume 4501 of Lecture Notes in Computer Science, pages 16–21. Springer Berlin Heidelberg, 2007. [4] Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, February 2009. ´ am Mann and Tam´ [5] Zolt´ an Ad´ as Szép. Accelerating backtrack search through a best-first-search strategy. Information Sciences, submitted. ´ am Mann and Tamás Szép. BCAT: A framework for analyzing the complexity of [6] Zolt´ an Ad´ algorithms. In Proceedings of the 8th IEEE International Symposium on Intelligent Systems and Informatics, pages 297–302, 2010. [7] Niklas Eén and Niklas S¨ orensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, SAT, volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer, 2003. ´ [8] Sz´ adeczky-Kardoss Ibolya Eva. szamitaselmelet.doc.

Szám´ıtáselmélet.

http://napszel.com/creations/szke_

[9] Carla P. Gomes, Bart Selman, and Henry A. Kautz. Boosting Combinatorial Search Through Randomization. In National Conference on Artificial Intelligence, pages 431–437, 1998. [10] Carla P. Gomes and David Shmoys. Completing quasigroups or latin squares: A structured graph coloring problem. In Proceedings of Computational Symposium on Graph Coloring and Generalizations, 2002. [11] Long Guo, Youssef Hamadi, Said Jabbour, and Lakhdar Sais. Diversification and intensification in parallel SAT solving. In David Cohen, editor, Principles and Practice of Constraint Programming – CP 2010, volume 6308 of Lecture Notes in Computer Science, pages 252–265. Springer Berlin Heidelberg, 2010. 39

Bart´ ok D´ avid


[12] Katona Gyula, Recski Andr´ as, and Szabó Csaba. A sz´ am´ıt´ astudom´ any alapjai. Typotex, 2002. [13] Henry Kautz, Eric Horvitz, Yongshao Ruan, Carla Gomes, and Bart Selman. Dynamic restart policies. In Eighteenth national conference on Artificial intelligence, pages 674–681, Menlo Park, CA, USA, 2002. American Association for Artificial Intelligence. [14] Inês Lynce and Jo˜ ao Marques-Silva. Efficient haplotype inference with boolean satisfiability. In Proceedings of the 21st national conference on Artificial intelligence - Volume 1, AAAI’06, pages 104–109. AAAI Press, 2006. [15] Jo˜ ao Marques-Silva. Practical applications of boolean satisfiability. In WODES 2008 : 9th International Workshop on Discrete Event Systems, pages 74–80, 2008. [16] Ruben Martins, Vasco Manquinho, and Inês Lynce. An overview of parallel SAT solving. Constraints, 17(3):304–347, 2012. [17] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: engineering an efficient SAT solver. In Proceedings of the 38th annual Design Automation Conference, DAC ’01, pages 530–535, New York, NY, USA, 2001. ACM. [18] Henry Yuen and Joseph Bebel. Tough SAT project. http://toughsat.appspot.com/.

40

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

Recommend Documents