haku: @keyword propositional satisfiability / yhteensä: 4
hakutulos-lista
viite: 3 / 4
« edellinen | seuraava »
Tekijä:Rantanen, Heikki
Työn nimi:Analyzing the Random-Walk Algorithm for SAT
Lauselogiikan toteutuvuusongelman satunnaiskulkualgoritmin analyyttinen tarkastelu
Julkaisutyyppi:Diplomityö
Julkaisuvuosi:2004
Sivut:7+47      Kieli:   eng
Koulu/Laitos/Osasto:Sähkö- ja tietoliikennetekniikan osasto
Oppiaine:Tietojenkäsittelyteoria   (T-119)
Valvoja:Niemelä, Ilkka
Ohjaaja:Niemelä, Ilkka
OEVS:
Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje
sulje

Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossa

Oppimiskeskuksen suljetussa verkossa voi lukea sellaisia digitaalisia ja digitoituja opinnäytteitä, joille ei ole saatu julkaisulupaa avoimessa verkossa.

Oppimiskeskuksen yhteystiedot ja aukioloajat: https://learningcentre.aalto.fi/fi/harald-herlin-oppimiskeskus/

Opinnäytteitä voi lukea Oppimiskeskuksen asiakaskoneilla, joita löytyy kaikista kerroksista.

Kirjautuminen asiakaskoneille

  • Aalto-yliopistolaiset kirjautuvat asiakaskoneille Aalto-tunnuksella ja salasanalla.
  • Muut asiakkaat kirjautuvat asiakaskoneille yhteistunnuksilla.

Opinnäytteen avaaminen

  • Asiakaskoneiden työpöydältä löytyy kuvake:

    Aalto Thesis Database

  • Kuvaketta klikkaamalla pääset hakemaan ja avaamaan etsimäsi opinnäytteen Aaltodoc-tietokannasta. Opinnäytetiedosto löytyy klikkaamalla viitetietojen OEV- tai OEVS-kentän linkkiä.

Opinnäytteen lukeminen

  • Opinnäytettä voi lukea asiakaskoneen ruudulta tai sen voi tulostaa paperille.
  • Opinnäytetiedostoa ei voi tallentaa muistitikulle tai lähettää sähköpostilla.
  • Opinnäytetiedoston sisältöä ei voi kopioida.
  • Opinnäytetiedostoa ei voi muokata.

Opinnäytteen tulostus

  • Opinnäytteen voi tulostaa itselleen henkilökohtaiseen opiskelu- ja tutkimuskäyttöön.
  • Aalto-yliopiston opiskelijat ja henkilökunta voivat tulostaa mustavalkotulosteita Oppimiskeskuksen SecurePrint-laitteille, kun tietokoneelle kirjaudutaan omilla Aalto-tunnuksilla. Väritulostus on mahdollista asiakaspalvelupisteen tulostimelle u90203-psc3. Väritulostaminen on maksullista Aalto-yliopiston opiskelijoille ja henkilökunnalle.
  • Ulkopuoliset asiakkaat voivat tulostaa mustavalko- ja väritulosteita Oppimiskeskuksen asiakaspalvelupisteen tulostimelle u90203-psc3. Tulostaminen on maksullista.
Sijainti:P1 Ark S80     | Arkisto
Avainsanat:propositional satisfiability
random-walk algorithm
probabilistic local search
simple random-walk
lauselogiikan toteutuvuus
satunnaiskulkualgoritmi
probabilistinen paikallinen haku
yksinkertainen satunnaiskulku
Tiivistelmä (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.
Tiivistelmä (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.
ED:2004-09-22
INSSI tietueen numero: 26318
+ lisää koriin
« edellinen | seuraava »
INSSI