2
0
Fork 0
mirror of https://github.com/MartinThoma/LaTeX-examples.git synced 2025-04-26 06:48:04 +02:00
This commit is contained in:
Martin Thoma 2013-09-07 15:25:30 +02:00
parent 03756e0131
commit 9cd9b55277
2 changed files with 5 additions and 3 deletions

Binary file not shown.

Before

Width:  |  Height:  |  Size: 57 KiB

After

Width:  |  Height:  |  Size: 64 KiB

Before After
Before After

View file

@ -28,10 +28,11 @@
\EndIf
\\
\State $P, Wert \gets \Call{FindeEinheitsklausel}{K, S, M}$
\LineComment{Eine Einheitsklausel hat nur ein Literal}
\State $K_i, P, Wert \gets \Call{FindeEinheitsklausel}{K, S, M}$
\If{$P$ existiert}
\State $M \gets \Call{SetzePInModell}{P, Wert, M}$
\State \Return $\Call{DPLL}{k, S \setminus \Set{P}, M}$
\State \Return $\Call{DPLL}{K \setminus \Set{K_i}, S \setminus \Set{P}, M}$
\EndIf
\\
@ -39,7 +40,8 @@
\LineComment{immer wahr bzw. immer falsch ist}
\State $P, Wert \gets \Call{FindeReinesLiteral}{K, M}$
\If{$P$ existiert}
\State $m \gets \Call{SetzePInModell}{P, Wert, M}$
\State $M \gets \Call{SetzePInModell}{P, Wert, M}$
\State $K \gets \Call{EntferneWahreKlauseln}{K, M}$
\State \Return $\Call{DPLL}{K, S \setminus \Set{P}, M}$
\EndIf
\\