Proof Complexity of Cut-Based Tableaux for Boolean Circuit Satisfiability Checking
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
v+56
Series
Abstract
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.Description
Supervisor
Niemelä, IlkkaThesis advisor
Junttila, TommiKeywords
propositional satisfiability, lauselogiikan toteutuvuusongelma, satisfiability checking, toteutuvuustarkastaminen, Boolean circuits, Boolen piirit, cut rule, leikkaussääntö, proof complexity, todistuskompleksisuus, polynomial simulation, polynominen simulointi, resolution, resoluutio, Davis-Putnam method, Davis-Putnam-menetelmä