haku: @instructor Junttila, Tommi / yhteensä: 6
viite: 6 / 6
« edellinen | seuraava »
Tekijä: | Järvisalo, Matti |
Työn nimi: | Proof Complexity of Cut-Based Tableaux for Boolean Circuit Satisfiability Checking |
Leikkaussääntöpohjaisten taulujen todistuskompleksisuus Boolen piirien toteutuvuustarkastamisessa | |
Julkaisutyyppi: | Diplomityö |
Julkaisuvuosi: | 2004 |
Sivut: | v+56 Kieli: eng |
Koulu/Laitos/Osasto: | Tietotekniikan osasto |
Oppiaine: | Tietojenkäsittelyteoria (T-119) |
Valvoja: | Niemelä, Ilkka |
Ohjaaja: | Junttila, Tommi |
OEVS: | Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossaOppimiskeskuksen 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
Opinnäytteen avaaminen
Opinnäytteen lukeminen
Opinnäytteen tulostus
|
Sijainti: | P1 Ark Aalto | Arkisto |
Avainsanat: | propositional satisfiability satisfiability checking Boolean circuits cut rule proof complexity polynomial simulation resolution Davis-Putnam method lauselogiikan toteutuvuusongelma toteutuvuustarkastaminen Boolen piirit leikkaussääntö todistuskompleksisuus polynominen simulointi resoluutio Davis-Putnam-menetelmä |
Tiivistelmä (fin): | Tämä työ käsittelee lauselogiikan toteutuvuusongelmaa. Tehokkaat toteutuvuustarkastimet perustuvat tyypillisesti Davis-Putnam-menetelmään, joka edellyttää syötteen olevan konjunktiivisessa normaalimuodossa. Tässä työssä tarkastellaan tästä poikkeavaa lähestymistapaa. Työssä esitellään yleisemmälle, Boolen piireiksi kutsutulle esitysmuodolle suunnattu taulumenetelmä. Menetelmää voidaan pitää Davis-Putnam-menetelmän yleistyksenä Boolen piireille. Työssä tarkastellaan leikkaussäännön käytön rajoittamisen vaikutusta taulumenetelmän tehokkuuteen todistuskompleksisuuden näkökulmasta. Toisin sanoen tarkastellaan, kuinka lyhyitä todistuksia on mahdollista tuottaa leikkaussäännön rajoitukset huomioonottaen. Työssä osoitetaan, että leikkaussäännön käytön rajoittaminen millä tahansa tarkastelluista tavoista kasvattaa todistuskompleksisuutta eksponentiaalisesti. Myös rajoitustapojen välillä osoitetaan olevan eksponentiaalisia eroja. Tulokset pohjautuvat konstruktiivisiin todistuksiin, joissa käytetään hyväksi muun muassa tunnettua kyyhkyslakkaperiaatetta ja menetelmien resoluutiorajoitteisuutta. Tulokset pätevät Davis-Putnam-menetelmään Tseitinin käännöksellä Boolen piireistä tuotettujen konjuktiivisessa normaalimuodossa olevien lauseiden osalta. Näin ollen työn tulokset osoittavat, että paikalliset leikkaussäännön rajoitukset Davis-Putnam-menetelmään perustuvissa toteutuvuustarkastimissa kasvattavat pahimmassa tapauksessa todistuksen kokoa eksponentiaalisesti. |
ED: | 2004-04-06 |
INSSI tietueen numero: 25120
+ lisää koriin
« edellinen | seuraava »
INSSI