Konjunktiivinen normaalimuoto ( CNF ) Boolen logiikassa on normaalimuoto , jossa Boolen kaava on muodoltaan literaalien disjunktioiden konjunktio . Konjunktiivinen normaalimuoto on kätevä automaattiseen lauseen todistamiseen . Mikä tahansa Boolen kaava voidaan muuntaa CNF:ksi. [1] Tähän voit käyttää: kaksoisnegaation lakia , de Morganin lakia , distributiivisuutta .
Kaavat CNF:ssä :
Kaavat , jotka eivät ole CNF :ssä :
Mutta nämä 3 kaavaa eivät vastaa CNF:n seuraavia kaavoja:
1) Päästä eroon kaikista kaavan sisältämistä loogisista operaatioista korvaamalla ne tärkeimmillä: konjunktiolla, disjunktiolla, negaatiolla. Tämä voidaan tehdä vastaavilla kaavoilla:
2) Korvaa koko lausekkeeseen viittaava kieltomerkki kieltomerkeillä, jotka viittaavat yksittäisiin muuttujalauseisiin kaavojen perusteella:
3) Päästä eroon kaksinkertaisista negatiivisista merkeistä.
4) Käytä tarvittaessa konjunktio- ja disjunktiooperaatioihin distributiivisuus- ja absorptiokaavojen ominaisuuksia.
Pelkistetään kaava muotoon CNF
Muunnetaan kaava kaavaksi, joka ei sisällä :
Tuloksena olevassa kaavassa siirrämme negaation muuttujiin ja vähennämme kaksoisnegatiointeja:
Jakelulain mukaan saamme CNF:
K -konjunktiivinen normaalimuoto on konjunktiivinen normaalimuoto, jossa jokainen disjunktio sisältää tarkalleen k literaalia .
Esimerkiksi seuraava kaava on kirjoitettu 2-CNF:llä:
Jos jokin muuttuja puuttuu yksinkertaisesta disjunktiosta (esimerkiksi z), lisäämme siihen lausekkeen: (tämä ei muuta itse disjunktiota), jonka jälkeen avataan hakasulkeet jakautumislain avulla :
Siten SKNF saadaan CNF:stä.
Seuraava muodollinen kielioppi kuvaa kaikki CNF:ksi pelkistetut kaavat:
<CNF> → <disjunkt> <CNF> → <CNF> ∧ <disjunkt> <disjunkt> → <kirjaimellinen>; <disjunct> → (<disjunkt> ∨ <kirjaimellinen>) <kirjaimellinen> → <termi> <kirjaimellinen> → ¬<termi>jossa <termi> tarkoittaa mielivaltaista loogista muuttujaa.
Laskennallisen monimutkaisuuden teoriassa tärkeä rooli on Boolen kaavojen tyydyttävyyden ongelmalla konjunktiivisessa normaalimuodossa. Cooken lauseen mukaan tämä ongelma on NP-täydellinen , ja se pelkistyy 3-CNF:n kaavojen tyydyttävyysongelmaksi, joka pienentää ja johon muut NP-täydelliset ongelmat puolestaan vähenevät .
2-CNF-kaavojen tyydyttävyysongelma voidaan ratkaista lineaarisessa ajassa.
On huomattava, että havainnoinnin helpottamiseksi aritmeettisen kertolasku- ja yhteenlaskumerkkejä käytetään usein konjunktion ja disjunktion nimityksinä, kun taas kertolasymboli jätetään usein pois. Tässä tapauksessa Boolen algebrakaavat näyttävät algebrallisilta polynomeilta, mikä on silmälle tutumpaa, mutta voi joskus johtaa väärinkäsityksiin.
Esimerkiksi seuraavat merkinnät ovat vastaavia:
Tästä syystä venäjänkielisessä kirjallisuudessa CNF:ää kutsutaan joskus "summien tuotteeksi", joka on piirrospaperi englanninkielisestä termistä "summien tuote".