search query: @instructor Niemelä, Ilkka / total: 15
reference: 5 / 15
« previous | next »
Author:Rantanen, Heikki
Title:Analyzing the Random-Walk Algorithm for SAT
Lauselogiikan toteutuvuusongelman satunnaiskulkualgoritmin analyyttinen tarkastelu
Publication type:Master's thesis
Publication year:2004
Pages:7+47      Language:   eng
Department/School:Sähkö- ja tietoliikennetekniikan osasto
Main subject:Tietojenkäsittelyteoria   (T-119)
Supervisor:Niemelä, Ilkka
Instructor:Niemelä, Ilkka
OEVS:
Electronic archive copy is available via Aalto Thesis Database.
Instructions

Reading digital theses in the closed network of the Aalto University Harald Herlin Learning Centre

In the closed network of Learning Centre you can read digital and digitized theses not available in the open network.

The Learning Centre contact details and opening hours: https://learningcentre.aalto.fi/en/harald-herlin-learning-centre/

You can read theses on the Learning Centre customer computers, which are available on all floors.

Logging on to the customer computers

  • Aalto University staff members log on to the customer computer using the Aalto username and password.
  • Other customers log on using a shared username and password.

Opening a thesis

  • On the desktop of the customer computers, you will find an icon titled:

    Aalto Thesis Database

  • Click on the icon to search for and open the thesis you are looking for from Aaltodoc database. You can find the thesis file by clicking the link on the OEV or OEVS field.

Reading the thesis

  • You can either print the thesis or read it on the customer computer screen.
  • You cannot save the thesis file on a flash drive or email it.
  • You cannot copy text or images from the file.
  • You cannot edit the file.

Printing the thesis

  • You can print the thesis for your personal study or research use.
  • Aalto University students and staff members may print black-and-white prints on the PrintingPoint devices when using the computer with personal Aalto username and password. Color printing is possible using the printer u90203-psc3, which is located near the customer service. Color printing is subject to a charge to Aalto University students and staff members.
  • Other customers can use the printer u90203-psc3. All printing is subject to a charge to non-University members.
Location:P1 Ark S80     | Archive
Keywords:propositional satisfiability
random-walk algorithm
probabilistic local search
simple random-walk
lauselogiikan toteutuvuus
satunnaiskulkualgoritmi
probabilistinen paikallinen haku
yksinkertainen satunnaiskulku
Abstract (eng): 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.
Abstract (fin): 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.
ED:2004-09-22
INSSI record number: 26318
+ add basket
« previous | next »
INSSI