Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
Download

📚 The CoCalc Library - books, templates and other resources

132938 views
License: OTHER
Tweet
Share
Share
1
\documentclass{article}

2
\usepackage[pdftex,active,tightpage]{preview}

3
\setlength\PreviewBorder{2mm}

4


5
\usepackage[utf8]{inputenc} % this is needed for umlauts

6
\usepackage[ngerman]{babel} % this is needed for umlauts

7
\usepackage[T1]{fontenc}    % this is needed for correct output of umlauts in pdf

8
\usepackage{amssymb,amsmath,amsfonts} % nice math rendering

9
\usepackage{braket} % needed for \Set

10
\usepackage{algorithm,algpseudocode}

11


12
\algnewcommand\True{\textbf{true}\space}

13
\algnewcommand\False{\textbf{false}\space}

14
\algnewcommand{\LineComment}[1]{\State \(\triangleright\) #1}

15
\begin{document}

16
\begin{preview}

17
    \begin{algorithm}[H]

18
        \begin{algorithmic}

19
            \Require Klauselmenge $K$, Symbolmenge $S$, (partielles) Modell $M$

20


21
			\Procedure{DPLL}{$K$, $S$, $M$}

22
            \If{Alle Klauseln sind wahr in $M$}

23
                \State \Return \texttt{true}

24
            \EndIf

25


26
            \If{Eine Klausel ist falsch in $M$}

27
                \State \Return \texttt{false}

28
            \EndIf

29
			\\

30


31
			\LineComment{Eine Einheitsklausel hat nur ein Literal}

32
            \State $K_i, P, Wert \gets \Call{FindeEinheitsklausel}{K, S, M}$

33
            \If{$P$ existiert}

34
                \State $M \gets \Call{SetzePInModell}{P, Wert, M}$

35
                \State \Return $\Call{DPLL}{K \setminus \Set{K_i}, S \setminus \Set{P}, M}$

36
            \EndIf

37
			\\

38


39
			\LineComment{Ein reines Literal ist eines, das in jeder Klausel}

40
			\LineComment{immer wahr bzw. immer falsch ist}

41
			\LineComment{Dieser Schritt ist der Grund,}

42
			\LineComment{warum DPLL nicht immer alle Lösungen findet}

43
            \State $P, Wert \gets \Call{FindeReinesLiteral}{K, M}$

44
            \If{$P$ existiert}

45
                \State $M \gets \Call{SetzePInModell}{P, Wert, M}$

46
				\State $K \gets \Call{EntferneWahreKlauseln}{K, M}$

47
                \State \Return $\Call{DPLL}{K, S \setminus \Set{P}, M}$

48
            \EndIf

49
			\\

50


51
            \State $P \gets S.pop()$ \Comment{Symbolmenge schrumpft}

52
            \State $M_1 \gets \Call{SetzePInModell}{P, \texttt{true}, M}$

53
            \State $M_2 \gets \Call{SetzePInModell}{P, \texttt{false}, M}$

54
            \State \Return $\Call{DPLL}{K, S, M_1} \lor \Call{DPLL}{K, S, M_2}$

55
			\EndProcedure

56
        \end{algorithmic}

57
    \caption{DPLL-Verfahren}

58
    \label{alg:dpll}

59
    \end{algorithm}

60
\end{preview}

61
\end{document}

62


63