Lauselogiikan toteutuvuusongelmaksi kutsutaan ongelmaa, jossa pyritään selvittämään, onko looginen lause toteutuva, eli tosi joillain sen propositiosymbolien totuusarvojen yhdistelmällä.
Esimerkiksi lause on toteutuva, koska lause on tosi, kun on tosi ja on epätosi. Yleensä lause, jolle ongelma pyritään ratkaisemaan, esitetään konjunktiivisessa normaalimuodossa.
Tietojenkäsittelytieteessä toteutuvuusongelma tunnetaan lyhenteellä SAT, ja sen tiedetään olevan yleisessä tapauksessa NP-täydellinen.Karp, Richard. Reducibility Among Combinatorial Problems. 1972. (englanniksi) Näin se on ratkaistavissa polynomisessa ajassa vain, jos P=NP. Tästä huolimatta on olemassa useampia heuristisia ratkaisimia, jotka kykenevät useissa tapauksissa ratkaisemaan toteutuvuusongelman käytännössä tuhansillakin symboleilla.Lintao, Zhang & Malik, Sharad. The quest for efficient boolean satisfiability solvers, Department of Electrical Engineering, Princeton University. 2002. Verkossa (englanniksi)
Lähteet
Luokka:Logiikka Luokka:Tietojenkäsittelyteoria