Konjunktiv normal form - Conjunctive normal form

I boolsk logik er en formel i konjunktiv normal form ( CNF ) eller klausulær normal form, hvis det er en sammenhæng af en eller flere klausuler , hvor en klausul er en adskillelse af bogstaver ; ellers er det et produkt af summer eller et OG af OR'er . Som en kanonisk normal form er den nyttig i automatiseret sætningsproevning og kredsløbsteori .

Alle sammenhænge af bogstaver og alle adskillelser af bogstaver er i CNF, da de kan ses som konjunktioner af henholdsvis en-bogstavede klausuler og sammenhænge af en enkelt klausul. Som i den disjunktive normale form (DNF) er de eneste propositionelle forbindelser, en formel i CNF kan indeholde, og og eller og ikke . Ikke -operatoren kan kun bruges som en del af en bogstavelig, hvilket betyder, at den kun kan gå forud for en propositionel variabel eller et prædikatsymbol .

I automatiseret sætningsbevis bruges begrebet " klausulær normalform " ofte i en snævrere forstand, hvilket betyder en særlig repræsentation af en CNF -formel som et sæt sæt bogstaver.

Eksempler og ikke-eksempler

Alle følgende formler i variablerne og er i konjunktiv normal form:

For klarhedens skyld er de adskilte klausuler skrevet inde i parentes ovenfor. I disjunktiv normal form med parenteserede konjunktivklausuler er det sidste tilfælde det samme, men det næstsidste er . Konstanterne sand og falsk betegnes med den tomme konjunkt og en klausul, der består af den tomme adskillelse, men er normalt skrevet eksplicit.

Følgende formler er ikke i konjunktiv normal form:

  • , da en OR er indlejret i et NOT
  • , da et OG er indlejret i et OR

Hver formel kan skrives tilsvarende som en formel i konjunktiv normal form. De tre ikke-eksempler i CNF er:

Konvertering til CNF

Hver propositionel formel kan konverteres til en ækvivalent formel, der er i CNF. Denne transformation er baseret på regler om logiske ækvivalenser : eliminering af dobbelt negation , De Morgans love og distributionsloven .

Da alle propositionelle formler kan konverteres til en ækvivalent formel i konjunktiv normal form, er beviser ofte baseret på den antagelse, at alle formler er CNF. I nogle tilfælde kan denne konvertering til CNF imidlertid føre til en eksponentiel eksplosion af formlen. For eksempel giver oversættelse af følgende ikke-CNF-formel til CNF en formel med klausuler:

Især den genererede formel er:

Denne formel indeholder klausuler; hver klausul indeholder enten eller for hver .

Der findes transformationer til CNF, der undgår en eksponentiel stigning i størrelse ved at bevare tilfredshed frem for ækvivalens . Disse transformationer vil garanteret kun øge formelens størrelse lineært, men introducere nye variabler. For eksempel kan ovenstående formel transformeres til CNF ved at tilføje variabler som følger:

En fortolkning opfylder kun denne formel, hvis mindst en af ​​de nye variabler er sand. Hvis denne variabel er , så er begge og også sande. Det betyder, at hver model, der opfylder denne formel, også opfylder den originale. På den anden side opfylder kun nogle af modellerne med den originale formel denne: Da de ikke er nævnt i den oprindelige formel, er deres værdier irrelevante for tilfredshed med den, hvilket ikke er tilfældet i den sidste formel. Det betyder, at den oprindelige formel og resultatet af oversættelsen er ligeværdige, men ikke ækvivalente .

En alternativ oversættelse, Tseitin -transformationen , omfatter også klausulerne . Med disse klausuler indebærer formlen ; denne formel anses ofte for at "definere" som et navn for .

Første ordens logik

I første ordens logik kan konjunktiv normal form tages yderligere for at give den klausulære normale form for en logisk formel, som derefter kan bruges til at udføre første ordens opløsning . I opløsningsbaseret, automatisk sætning, en CNF-formel

, med bogstaver, er almindeligt repræsenteret som et sæt sæt
.

Se et eksempel nedenfor .

Beregningskompleksitet

Et vigtigt sæt problemer i beregningskompleksitet involverer at finde tildelinger til variablerne i en boolsk formel udtrykt i konjunktiv normal form, således at formlen er sand. Den k -Sat problem er problemet med at finde en tilfredsstillende opgave til en boolsk formel udtrykt i CNF hvori hver disjunktion indeholder højst k variabler. 3-SAT er NP-komplet (ligesom ethvert andet k -SAT-problem med k > 2), mens 2-SAT er kendt for at have løsninger i polynomtid . Som en konsekvens er opgaven med at konvertere en formel til en DNF , bevare tilfredshed, NP-hård ; duelt , omdannes til CNF, bevare gyldighed , er også NP-hårde; derfor er ækvivalensbevarende omdannelse til DNF eller CNF igen NP-hård.

Typiske problemer i dette tilfælde involverer formler i "3CNF": konjunktiv normal form med ikke mere end tre variabler pr. Konjunkt. Eksempler på sådanne formler, man støder på i praksis, kan være meget store, for eksempel med 100.000 variabler og 1.000.000 konjunktioner.

En formel i CNF kan konverteres til en equisatisfiable formel i " k CNF" (for k ≥3) ved at udskifte hver konjunkt med mere end k variabler med to konjunkturer og med Z en ny variabel, og gentage så ofte som nødvendigt.

Konvertering fra første ordens logik

Sådan konverteres førsteordens logik til CNF:

  1. Konverter til negation normal form .
    1. Fjern konsekvenser og ækvivalenser: udskift gentagne gange med ; erstatte med . Til sidst vil dette fjerne alle forekomster af og .
    2. Flyt NOTs indad ved gentagne gange at anvende De Morgans lov . Specifikt erstattes med ; erstatte med ; og erstat med ; erstatte med ; med . Derefter kan a kun forekomme umiddelbart før et prædikatsymbol.
  2. Standardiser variabler
    1. For sætninger som bruger det samme variabelnavn to gange, skal du ændre navnet på en af ​​variablerne. Dette undgår forvirring senere, når du slipper kvantificatorer. For eksempel omdøbes til .
  3. Skolemize udsagnet
    1. Flyt kvantificatorer udad: udskift gentagne gange med ; erstatte med ; erstatte med ; erstatte med . Disse udskiftninger bevarer ækvivalens, da det foregående variable standardiseringstrin sikrede, at det ikke forekommer i . Efter disse udskiftninger, kan der forekomme en kvantifikator kun i den indledende præfiks med formlen, men aldrig inde i en , eller .
    2. Skift gentagne gange med , hvor er et nyt -ary -funktionssymbol, en såkaldt " Skolem -funktion ". Dette er det eneste trin, der kun bevarer tilfredshed frem for ækvivalens. Det eliminerer alle eksistentielle kvantificatorer.
  4. Drop alle universelle kvantificatorer.
  5. Fordel OR'er indad over AND'er: udskift gentagne gange med .

Som et eksempel, formlen siger "Enhver, som elsker alle dyr, er til gengæld elsket af nogen" omdannes til CNF (og efterfølgende i klausul formularen i sidste linje) som følger (fremhæve udskiftning rule redexes i ):

med 1.1
med 1.1
med 1.2
med 1.2
med 1.2
med 2
med 3.1
med 3.1
med 3.2
af 4
med 5
( klausul repræsentation)

Uformelt kan Skolem -funktionen betragtes som at give den person, som er elsket, mens den giver det dyr (hvis nogen), der ikke elsker. Den tredje sidste linje nedenunder lyder derefter som " elsker ikke dyret , eller også er det elsket af " .

Den 2. sidste linje ovenfra , er CNF.

Noter

  1. ^ Peter B. Andrews, En introduktion til matematisk logik og typeteori ,2013, ISBN  9401599343 , s. 48
  2. ^ a b Kunstig intelligens: En moderne tilgang Arkiveret 2017-08-31 på Wayback Machine [1995 ...] Russell og Norvig
  3. ^ Tseitin (1968)
  4. ^ Jackson og Sheridan (2004)
  5. ^ da en måde at kontrollere en CNF for tilfredshed er at konvertere den til en DNF , hvis tilfredshed kan kontrolleres i lineær tid

Se også

Referencer

eksterne links