Lauselogiikka (Boolen logiikka) on keskeinen esim. matemaattisen päättelyn ja digitaalipiirien suunnittelun pohjana oleva looginen kalkyyli. Monet lauselogiikan sovellutukset palautuvat viimekädessä toteutuvuusongelmaan: löytyykö annetun lauselogiikan lauseen (Boolen lausekkeen) atomisille muuttujille totuusarvot siten, että lause toteutuu.
Lauselogiikka on tärkeä työkalu tietojenkäsittelytekniikassa esimerkiksi laskennallisen vaativuuden teoriassa, ohjelmointikielissä ja tietokannoissa. Juuri lauselogiikan toteutuvuusongelma tunnistettiin ensimmäisenä ns. NP-täydelliseksi ongelmaksi. Nykyään tähän laskennallisesti vaikeiden ongelmien luokkaan tiedetään kuuluvan valtava määrä käytännön insinöörityössä esiintulevia laskennallisesti haastavia tehtäviä.
Lauselogiikan toteutuvuusongelma onkin eräs tietojenkäsittelytekniikan tutkituimpia kysymyksiä. Sen tutkimus on auttanut ymmärtämään paremmin vaikeiden laskennallisten ongelmien luonnetta, esim. ns. faasimuutosilmiötä. Aivan viime vuosina toteutuvuusongelman ratkaisumenetelmät ovat kehittyneet huimaa tahtia. Toisaalta on kehitetty uusia heuristiikkoja, hakuavaruuden karsintamenetelmiä ja toteutustekniikkaa ja toisaalta mielenkiintoisia paikalliseen stokastiseen hakuun perustuvia menetelmiä, joissa ideoita on haettu esim. tilastollisesta fysiikasta. Tuloksena on syntynyt useita tehokkaita toteutuksia, jotka kykenevät ratkaisemaan satoja tuhansia lausemuuttujia sisältäviä ongelmia. Pisimmällä lauselogiikan teolliset sovellutukset ovat laitteistosuunnittelussa ja testigeneroinnissa. Tämäntyyppisissä tehtävissä toteutuvuustarkastimista onkin muodostumassa keskeinen työkalu. Menetelmien nopea kehitys mahdollistaa jatkuvasti uusia sovellutusalueita, joista mainittakoon ohjelmistojärjestelmien suunnittelu ja verifiointi sekä tekoäly- ja tietämystekniikkasovellutukset.
Seminaarin tarkoituksena on perehtyä lauselogiikan lupaavimpiin toteutuvuustarkastusmenetelmiin, niiden taustalla olevaan teoriaan, toteutustekniikkaan ja suorituskykyyn käymällä läpi alueen keskeisiä uusi tuloksia tutkimusseminaarimuotoisesti.