Väitös tietotekniikan alalta, DI Jori Bomanson

Väitöskirjan nimi on "Normalization and Rewriting for Answer Set Programming and Optimization”

Sääntöpohjainen rajoiteohjelmointi on tietojenkäsittelytieteeseen ja ohjelmointikehitykseen pohjautuva ratkaisumenetelmä kombinatorisille haku- ja optimointiongelmille. Tällaisiksi ongelmiksi lukeutuvat esimerkiksi sellaiset aikataulutus-, konfigurointi-, resurssienjako- ja optimointiongelmat, joissa päähaasteena on monien valintojen teko niin, että niistä muodostuu säännönmukainen kokonaisuus. Kombinatoriset ongelmat ylittävät ajoittain tehokkaimpienkin tietokoneiden ratkaisukyvyn. Siksi on tärkeää tehostaa älykkäitä ratkaisumenetelmiä, kuten sääntöpohjaista rajoiteohjelmointia.

Tässä väitöskirjassa kehitettiin tehokkuutta parantavia menetelmiä sääntöpohjaiselle rajoiteohjelmoinnille ja saavutettiin muun muassa korkein optimointitehokkuus eräässä alalla pidetyssä kansainvälisessä kilpailussa. Kehitetyt menetelmät perustuvat automaattisiin ohjelmamuunnoksiin. Nämä ohjelmamuunnokset tuovat esille ohjelmien loogista rakennetta muodossa, joka parhaimmillaan edesauttaa ongelmanratkontaa merkittävästi. Ratkaisutehoon keskittyvän käytännönläheisen työn tueksi väitöskirjassa kehitettiin uusia formaaleja menetelmiä ohjelmamuunnosten oikeellisuuden analysoimiseksi ja varmistamiseksi.

Vastaväittäjä: professori Yuliya Lierler, The University of Nebraska Omaha, USA

Kustos: professori Ilkka Niemelä, Aalto-yliopiston perustieteiden korkeakoulu, tietotekniikan laitos

Väittelijän yhteystiedot: Jori Bomanson, tietotekniikan laitos, p. 050 5058809, [email protected]

Väitös järjestetään etäyhteyden kautta. Linkki väitökseen (Zoom)

Väitöskirja on julkisesti nähtävillä 10 päivää ennen väitöstä Aalto-yliopiston julkaisuarkistossa (aaltodoc.aalto.fi).

Elektroninen väitöskirja (aaltodoc.aalto.fi)