Cube and Conquer example
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}
|
Relevante Bilder
Relevante Artikel
Erfüllbarkeitsproblem der AussagenlogikDas 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