Nächste Seite:
Modellierung durch SAT
Aufwärts:
Erfüllbarkeit aussagenlogischer Formeln (SAT)
Vorherige Seite:
Der Folgerungsbegriff
Normalformen (DNF, CNF)
Definitionen:
Variable:
v
1
,…
Literal:
v
oder
¬
v
DNF-Klausel: Konjunktion von Literalen
DNF-Formel: Disjunktion von DNF-Klauseln
CNF-Klausel: Disjunktion von Literalen
CNF-Formel: Konjunktion von CNF-Klauseln
Disjunktion als Implikation: diese Formeln sind äquivalent:
(
x
1
∧…∧
x
m
)→(
y
1
∨…∨
y
n
)
(¬
x
1
∨…∨¬
x
m
∨
y
1
∨…∨
y
n
)
2014-07-06
