Cube and Conquer example


Autor/Urheber:
Vwinkler
Attribution:
Das Bild ist mit 'Attribution Required' markiert, aber es wurden keine Informationen über die Attribution bereitgestellt. Vermutlich wurde bei Verwendung des MediaWiki-Templates für die CC-BY Lizenzen der Parameter für die Attribution weggelassen. Autoren und Urheber finden für die korrekte Verwendung der Templates hier ein Beispiel.
Shortlink:
https://www.dewiki.de/b/2108a7
Quelle:
Wikimedia Commons
Größe:
1496 x 753 Pixel (22926 Bytes)
Beschreibung:
Solving a SAT instance applying the Cube and Conquer paradigm

Illustration of the decisions made by the look-ahead phase and the five resulting cubes. Decision heuristics choose the variables (circles). Cutoff heuristics choose when to stop dividing the problem. CDCL solvers will then solve the partial problems (rectangles) independently.

Source Code
\documentclass[tikz,convert={outfile=\jobname.svg}]{standalone} 
\usetikzlibrary{trees}

\begin{document}
\begin{tikzpicture}[grow=right,
level 1/.style={sibling distance=3cm,level distance=2cm},
level 2/.style={sibling distance=1.5cm,level distance=3cm},
level 3/.style={sibling distance=1.5cm,level distance=3cm},
every internal node/.style={circle,draw},
every leaf node/.style={rectangle,draw}
]

\node (Root) [circle,draw] {$x_4$}
child {
    node (A) [circle,draw] {$x_8$}
    child { node (B) [rectangle,draw] {$F \wedge (\neg x_4 \wedge \neg x_8)$ } }
    child {
        node  (C) [circle,draw] {$x_9$}
        child {
            node (D) [rectangle,draw] {$F \wedge (\neg x_4 \wedge x_8 \wedge \neg x_9)$ }
        }
        child {
            node (E) [rectangle,draw] {$F \wedge (\neg x_4 \wedge x_8 \wedge x_9)$ }
        }
    }
}
child {
    node (F) [circle,draw] {$x_1$}
    child { node (G) [rectangle,draw] {$F \wedge (x_4 \wedge \neg x_1)$ } }
    child { node (H) [rectangle,draw] {$F \wedge (x_4 \wedge x_1)$ } }
};

\begin{scope}[nodes = {draw = none}]
    \path (Root) -- (A) node [near start, below]  {$0$};
    \path (A)     -- (B) node [near start, below]  {$0$};
    \path (A)     -- (C) node [near start, above] {$1$};
    \path (C)     -- (D) node [near start, below] {$0$};
    \path (C)     -- (E) node [near start, above] {$1$};
    \path (Root) -- (F) node [near start, above] {$1$};
    \path (F)     -- (G) node [near start, below]  {$0$};
    \path (F)     -- (H) node [near start, above] {$1$};
\end{scope}
\end{tikzpicture}
\end{document}
Lizenz:
CC BY-SA 4.0
Bild teilen:
Facebook   Twitter   Pinterest   WhatsApp   Telegram   E-Mail
Weitere Informationen zur Lizenz des Bildes finden Sie hier. Letzte Aktualisierung: Sun, 18 May 2025 22:58:10 GMT

Relevante Bilder


Relevante Artikel

Erfüllbarkeitsproblem der Aussagenlogik

Das Erfüllbarkeitsproblem der Aussagenlogik ist ein Entscheidungsproblem der theoretischen Informatik. Es beschäftigt sich mit der Frage, ob eine gegebene aussagenlogische Formel erfüllbar ist. Mit anderen Worten: Existiert eine Belegung der Variablen von mit den Werten wahr oder falsch, sodass zu wahr ausgewertet wird? .. weiterlesen