This is an old revision of the document!
Propositionallogik
Syntax
| Propositionale Variablen | $A, B, C, \ldots$ |
| Junktoren | $\neg, \wedge, \vee, \Rightarrow, \Leftrightarrow$ |
| Formel | $\phi, \psi, \ldots$ |
| Konstanten | $\top, \perp$ |
Semantik
| Belegung | $\eta$ |
| Foo | $⟦\phi⟧\eta$ |
| Bar | $\&, \mid\mid$ |
| Tautologie | $\forall \eta:⟦\phi⟧\eta$ |
| Erfüllbar | $\exists \eta:⟦\phi⟧\eta$ |
| Unerfüllbar | $\forall \eta:\neg⟦\phi⟧\eta$ |
| Äquivalent | $\forall \eta:⟦\phi⟧\eta = ⟦\psi⟧\eta$ |
| Erfüllbarkeitsäuivalenz | $(\phi \text{ und } \psi \text{ sind erfüllbar}) \vee (\phi \text{ und } \psi \text{ sind unerfüllbar})$ |
Normierung
| Literal | $A$ und $\neg A$ |
| Minterm | Konjunktion: $\ldots \wedge \ldots \wedge \ldots \wedge \ldots$ (Die wenigsten Belegungen sind $\top$) |
| Maxterm / Klausel | Disjunktion: $\ldots \vee \ldots \vee \ldots \vee \ldots$ (Die meisten Belegungen sind $\top$) |
| KNF | $(\ldots \vee \ldots \vee \ldots \vee \ldots ) \wedge ( \ldots \vee \ldots \vee \ldots \vee \ldots )$ |
| DNF | $(\ldots \wedge \ldots \wedge \ldots \wedge \ldots) \vee (\ldots \wedge \ldots \wedge \ldots \wedge \ldots)$ |
| $\phi$ … KNF | Größe | Zeit |
| Äquivalent | exponentiell | ? |
| Erfüllungsäuivalent | linear | polynomiell |
Tseitin Übersetzung
| $$KNF(A) = (A, \top)$$ |
| $$\begin{array}{ll}KNF(\neg\phi) =&\text{let } (B, \Gamma) = KNF(\phi) \text{ in} \\ & (C, \Gamma \wedge (C \vee B) \wedge (\neg C \vee \neg B))\end{array}$$ |
| $$\begin{array}{ll}KNF(\phi_1\vee\phi_2) =&\text{let } (B_1, \Gamma_1) = KNF(\phi_1) \text{ in} \\ &\text{let } (B_2, \Gamma_2) = KNF(\phi_2) \text{ in} \\ & (C, \Gamma_1 \wedge \Gamma_2 \wedge (\neg C \vee B_1 \vee B_2) \wedge (C \vee \neg B_1) \wedge (C \vee \neg B_2))\end{array}$$ |
SAT-Solver
