Automatisoitu päättely toteutuvuustarkistimilla

Abstract

Toteutuvuustarkistimet ovat tietokoneohjelmia, jotka ratkaisevat lauselogiikan toteutuvuusongelman annetulle logiikan lauseelle, eli ne selvittävät, onko lause missään tapauksessa tosi. Toteutuvuuden selvittäminen on tunnetusti NP-täydellinen ongelma. Tästä huolimatta toteutuvuustarkistimien käytännön tehokkuus on vuosien kehityksen myötä kasvanut huomattavasti. Toteutuvuustarkistimia voidaan hyödyntää käytännön sovelluksissa, sillä moni vaikea laskennallinen ongelma on muunnettavissa toteutuvuusongelmaksi ja tällöin ratkaistavissa käytännöllisessä ajassa toteutuvuustarkistimella. Lauselogiikkaa voidaan siis käyttää mallintamaan ongelmia ja toteutuvuustarkistimia ratkaisemaan niitä.

Tutkielman ensimmäinen osa keskittyy toteutuvuustarkistimien teorian perusteisiin eli lauselogiikan määritelmiin ja yksinkertaisiin algoritmeihin sekä kertoo lyhyesti toteutuvuustarkistimien tehokkuuden kehityksestä. Jälkimmäisessä osassa tutustutaan toteutuvuustarkistimien sovelluksiin ja käydään läpi näiden toimintaperiaatteita loogisen mallinnuksen ja automatisoidun päättelyn näkökulmasta. Tarkasteltavat sovellukset ovat reittien suunnittelu graafeissa, matemaattisten todistusten tekeminen, rautateiden suunnittelu ja junaliikenteen ohjaus sekä digitaalipiirien suunnittelu ja verifiointi. Sovelluksien mielekkyydestä ja tulevaisuuden odotuksista keskustellaan erityisesti verrattuna vaihtoehtoisiin ratkaisumenetelmiin. Tutkittavaksi valituissa sovelluksissa ratkaistaan käytännöllisiä tai muusta syystä mielenkiintoisia ongelmia siten, että ratkaisun tehokkuus ja käytettävyys on kilpailukykyinen toteutuvuustarkistimia hyödyntämättömiin vaihtoehtoihin nähden.

Toteutuvuustarkistimien soveltamisen nähdään olevan tehokas ja edelleen kehittyvä tapa ratkaista erinäisiä ongelmia. Toisaalta sovelluksiin liittyy haasteita. Alkuperäisen ongelman muuntaminen toteutuvuusongelmaksi vie aikaa ja kadottaa ongelman rakennetta. Lisäksi ongelmat, joihin sovellukset kohdistuvat, ovat tyypillisesti itsessään vaativia.