Jump to content

File:Cube and Conquer example.svg

Page contents not supported in other languages.
This is a file from the Wikimedia Commons
From Wikipedia, the free encyclopedia
    Original file (SVG file, nominally 1,496 × 753 pixels, file size: 22 KB)

    Summary

    Description
    English: 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}
    
    Date
    Source Own work
    Author Vwinkler
    SVG development
    InfoField
     The SVG code is valid.
     This vector image was created with Potrace.

    Licensing

    I, the copyright holder of this work, hereby publish it under the following license:
    w:en:Creative Commons
    attribution share alike
    This file is licensed under the Creative Commons Attribution-Share Alike 4.0 International license.
    You are free:
    • to share – to copy, distribute and transmit the work
    • to remix – to adapt the work
    Under the following conditions:
    • attribution – You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
    • share alike – If you remix, transform, or build upon the material, you must distribute your contributions under the same or compatible license as the original.

    Captions

    Add a one-line explanation of what this file represents

    Items portrayed in this file

    depicts

    15 February 2020

    image/svg+xml

    9b2b005704216fac61aaf22261cb1671ab3b1c54

    22,926 byte

    753 pixel

    1,496 pixel

    File history

    Click on a date/time to view the file as it appeared at that time.

    Date/TimeThumbnailDimensionsUserComment
    current17:06, 15 February 2020Thumbnail for version as of 17:06, 15 February 20201,496 × 753 (22 KB)VwinklerCross-wiki upload from en.wikipedia.org

    The following 2 pages use this file:

    Global file usage

    The following other wikis use this file:

    Metadata