Lauselogiikan toteutuvuusongelma

Lauselogiikan toteutuvuusongelmaksi kutsutaan ongelmaa, jossa pyritään selvittämään, onko looginen lause toteutuva, eli tosi joillain sen propositiosymbolien totuusarvojen yhdistelmällä.

Esimerkiksi lause $p_{0} \land \neg p_{1}$ on toteutuva, koska lause on tosi, kun $p_{0}$ on tosi ja $p_{1}$ 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.^[1] 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.^[2]

Lähteet

Malline:Viitteet

Malline:Tynkä/Matematiikka

↑ Karp, Richard. Reducibility Among Combinatorial Problems. 1972. (englanniksi)
↑ Lintao, Zhang & Malik, Sharad. The quest for efficient boolean satisfiability solvers, Department of Electrical Engineering, Princeton University. 2002. Verkossa (englanniksi)

[1] Karp, Richard. Reducibility Among Combinatorial Problems. 1972. (englanniksi)

[2] Lintao, Zhang & Malik, Sharad. The quest for efficient boolean satisfiability solvers, Department of Electrical Engineering, Princeton University. 2002. Verkossa (englanniksi)

[1]

[2]

Lauselogiikan toteutuvuusongelma

Lähteet

Navigointivalikko

Haku