Lauselogiikan toteutuvuustarkistimen laajentaminen pariteettipäättelyllä

Tero Laitinen

    Tutkimustuotos: Doctoral ThesisCollection of Articles

    Abstrakti

    Hakukonflikteista oppivia lauselogiikan toteutuvuustarkastimia on menestyksekkäästi sovellettu ongelmanratkaisuun useissa käytännön sovellutuksissa. Tietyillä sovellusalueilla, kuten piiriverifiointi, rajoitettu mallintarkastus, looginen kryptoanalyysi ja approksimoiva ratkaisumallien lukumäärän laskenta, ongelmakuvauksien vaatimuksia voidaan ilmaisuvoimaisesti mallintaa pariteettirajoitteilla. Ongelmat, jotka sisältävät pariteetti- eli xor-rajoitteita, voivat tosin olla erityisen vaativia toteutuvuustarkistimille, jotka käsittelevät ongelmaa konjunktiivisessa normaalimuodossa. Tässä väitöskirjassa tutkitaan, miten hakukonflikteista oppivia toteutuvuustarkistimia voidaan kehittää käsittelemään pariteettirajoitteita sisältäviä ongelmia käyttäen aikaisemmin julkaistua DPLL(XOR)-hakumenetelmäkehystä, jossa toteutuvuustarkistimeen yhdistetään pariteettirajoitteita käsittelevä ratkaisinmoduuli. Työssä esitellään erilaisia pariteettipäättelyjärjestelmiä kuten yksikköpropagaatio, ekvivalenssipäättely ja täydellisen pariteettipäättelyn tuottava inkrementaalinen Gauss-Jordan-eliminaatio. Pariteettirajoitejohtoihin perustuvien pariteettipäättelyjärjestelmien analysoimiseksi esitellään tekniikoita, joilla voidaan johtaa lyhyempiä klausuulipohjaisia selityksiä implikoiduille literaaleille ja joita voidaan käyttää uusien pariteettirajoitteiden oppimiseksi hakukonfliktien käsittelyn yhteydessä. Työssä osoitetaan, että näillä tekniikoilla voidaan simuloida täydellistä pariteettipäättelyjärjestelmää rajatussa ongelmajoukossa ja niiden avulla voidaan tuottaa lyhyitä ongelman toteutumattomuuden osoittavia todistuksia eräille ongelmille, joiden kuvaukset konjunktiivisessa normaalimuodossa ovat vaikeita resoluutiolle. Väitöskirjassa käsitellään approksimoivia luokittelumenetelmiä, joilla voidaan päätellä, että annetulle ongelmalle riittää käyttää yksikköpropagaatiota tai ekvivalenssipäättelyä kaikkien implikoitujen literaalien päättelyyn. Työssä näytetään, miten erilaisia menetelmiä osittaa ongelma erillisiksi aliongelmiksi voidaan soveltaa pariteettirajoitejoukkoihin. Ositusmenetelmiä voidaan käyttää pienentämään Gauss-Jordan eliminaatiossa käytettävien matriisien kokoa, kun käytetään tiivistä matriisiesitystä, ja jokaiselle ositetulle aliongelmalle voidaan valita sopiva pariteettipäättelyjärjestelmä. Pariteettipäättelyn simulointia tutkitaan käyttäen ekvivalenssipäättelyä ja vahvempaa pariteettipäättelyä simuloivia käännöksiä, jotka mahdollistavat olemassa olevien toteutuvuustarkistimien hyödyntämisen. Työssä osoitetaan, että ekvivalenssipäättelyä voidaan simuloida lisäämällä polynominen määrä ylimääräisiä pariteettirajoitteita, mutta ilman lisämuuttujia tarvitaan eksponentiaalinen määrä pariteettirajoitteita pahimmassa tapauksessa. Työssä näytetään, että resoluutio simuloi ekvivalenssipäättelyä tehokkaasti. Esiteltyjä tekniikoita arvioidaan kokeellisesti monilla haastavilla ongelmilla, jotka on tuotettu salausmenetelmistä ja SAT Competitionkilpailuongelmista.
    Julkaisun otsikon käännösLauselogiikan toteutuvuustarkistimen laajentaminen pariteettipäättelyllä
    AlkuperäiskieliEnglanti
    PätevyysTohtorintutkinto
    Myöntävä instituutio
    • Aalto-yliopisto
    Valvoja/neuvonantaja
    • Niemelä, Ilkka, Valvoja
    • Junttila, Tommi, Ohjaaja
    Kustantaja
    Painoksen ISBN978-952-60-5944-0
    Sähköinen ISBN978-952-60-5945-7
    TilaJulkaistu - 2014
    OKM-julkaisutyyppiG5 Tohtorinväitöskirja (artikkeli)

    Tutkimusalat

    • lauselogiikan toteutuvuusongelma
    • pariteettipäättely

    Sormenjälki Sukella tutkimusaiheisiin 'Lauselogiikan toteutuvuustarkistimen laajentaminen pariteettipäättelyllä'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

    Siteeraa tätä