Analyzing the Random-Walk Algorithm for SAT
No Thumbnail Available
URL
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology |
Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Authors
Date
2004
Department
Major/Subject
Tietojenkäsittelyteoria
Mcode
T-119
Degree programme
Language
en
Pages
7+47
Series
Abstract
The propositional logic satisfiability (SAT) problem has gained growing interest in recent years. From complexity theory is known that many real-world mathematical and engineering problems can be translated into SAT problem instances. Advances on SAT solution algorithms in the past ten or fifteen years have enabled solving these problems by a computer. This, for one, has inspired developing even better algorithms. In this work we study the so-called random-walk algorithm, which is a well-known probabilistic solution method for the SAT problem. The aim is to give insight into the algorithm with analytical methods and answer some open questions. For example, one would like to know the optimal value for the restart-moment-a parameter that has notable effect on the algorithm's performance. The analysis leads to a stochastic model that is a Markov chain; more precisely a simple random-walk between an absorbing and a reflecting barrier. A scheme to solve the problem for fixed number of variables is obtained from the theory of Markov chains. In general case, however, things get more complicated. Namely such a random-walk, despite its simplicity, shows very complex behaviour and unfortunately no closed-form solution formula is known. Consequently, one must abide by approximatively results. The contribution of this work includes solving the optimal restart moment approximately and a rigorous performance analysis. The calculations give insight into the algorithm's nature underlining the importance of restarts. Also some experimental study is made, and the results support the developed stochastic model.Lauselogiikan toteutuvuuden (SAT) ongelmaa on tutkittu viime vuosina kasvavassa määrin. Kompleksisuusteoriasta tiedämme, että useat käytännön matemaattiset ja tekniset ongelmat voidaan muuntaa vastaamaan SAT-ongelmaa. SAT-ongelman ratkaisumenetelmien 10 - 15 viime vuoden aikana tapahtuneen kehityksen ansiosta naita ongelmia voidaan ratkoa tietokoneella. Tämä puolestaan on innostanut kehittämään yhä parempia menetelmiä. Työssä tutkitaan niin kutsuttua satunnaiskulkualgoritmia, joka on tunnettu probabilistinen SAT-ongelman ratkaisumenetelmä. Työn tarkoituksena on analyyttisen tarkastelun avulla auttaa ymmärtämään algoritmin luonteenpiirteet ja vasta eräisiin avoimiin kysymyksiin. Yksi tällainen kysymys liittyy algoritmin suorituskyvyn maksimointiin uudelleenkäynnistysten avulla - optimaalista hetkeä uudelleenkäynnistykselle ei tiedetä. Analyysin tuloksena saadaan stokastinen malli, joka on luonteeltaan Markovin ketju, tarkemmin sanottuna yksinkertainen satunnaiskulku absorboivan ja heijastavan seinän välillä. Ratkaisumalli kiinnitetyn muuttujamäärän tapauksessa saadaan suoraan Markovin ketjujen teoriasta. Yleisessä tapauksessa kuitenkin törmätään vaikeuksiin. Kyseisen satunnaiskulun käytös on nimittäin yllättävän kompleksinen, eikä selkeää suljetun muodon ratkaisua tunneta. Tarvitaan siis approksimoivia menetelmiä. Työn keskeiset tulokset ovat algoritmin optimaalisen uudelleenkäynnistysajankohdan ratkaiseminen approksimatiivisesti ja suorituskyvyn täsmällinen analyysi. Esitetty matemaattinen analyysi auttaa ymmärtämään algoritmin luonteenpiirteitä; se mm. korostaa uudelleenkäynnistysten merkitystä. Lopun kokeelliset tulokset näyttävät tukevan kehitettyä stokastista mallia.Description
Supervisor
Niemelä, IlkkaThesis advisor
Niemelä, IlkkaKeywords
propositional satisfiability, lauselogiikan toteutuvuus, random-walk algorithm, satunnaiskulkualgoritmi, probabilistic local search, probabilistinen paikallinen haku, simple random-walk, yksinkertainen satunnaiskulku