search query: @keyword resolution / total: 4
reference: 2 / 4
Author: | Järvisalo, Matti |
Title: | Proof Complexity of Cut-Based Tableaux for Boolean Circuit Satisfiability Checking |
Leikkaussääntöpohjaisten taulujen todistuskompleksisuus Boolen piirien toteutuvuustarkastamisessa | |
Publication type: | Master's thesis |
Publication year: | 2004 |
Pages: | v+56 Language: eng |
Department/School: | Tietotekniikan osasto |
Main subject: | Tietojenkäsittelyteoria (T-119) |
Supervisor: | Niemelä, Ilkka |
Instructor: | Junttila, Tommi |
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 CentreIn 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
Opening a thesis
Reading the thesis
Printing the thesis
|
Location: | P1 Ark Aalto | Archive |
Keywords: | 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ä |
Abstract (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 record number: 25120
+ add basket
INSSI