50 lines
4.4 KiB
XML
50 lines
4.4 KiB
XML
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||
|
|
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
|
||
|
|
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
|
||
|
|
<!-- Generated by graphviz version 14.1.2 (20260126.1125)
|
||
|
|
-->
|
||
|
|
<!-- Title: d09 Pages: 1 -->
|
||
|
|
<svg width="393pt" height="321pt"
|
||
|
|
viewBox="7.00 7.00 386.00 314.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
|
||
|
|
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(11.2 310.04)">
|
||
|
|
<title>d09</title>
|
||
|
|
<!-- store -->
|
||
|
|
<g id="node1" class="node">
|
||
|
|
<title>store</title>
|
||
|
|
<path fill="#eef2ff" stroke="#4338ca" stroke-width="2" d="M290.3,-298.84C290.3,-298.84 80.63,-298.84 80.63,-298.84 74.63,-298.84 68.63,-292.84 68.63,-286.84 68.63,-286.84 68.63,-246.56 68.63,-246.56 68.63,-240.56 74.63,-234.56 80.63,-234.56 80.63,-234.56 290.3,-234.56 290.3,-234.56 296.3,-234.56 302.3,-240.56 302.3,-246.56 302.3,-246.56 302.3,-286.84 302.3,-286.84 302.3,-292.84 296.3,-298.84 290.3,-298.84"/>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="111.96" y="-278.85" font-family="DejaVu Sans" font-weight="bold" font-size="13.00" fill="#4338ca">CONSTRAINT STORE</text>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="81.59" y="-254.7" font-family="DejaVu Sans" font-size="10.00" fill="#1a1a2e">Domain x₁ ∈ {1, 2, 3, 4},  x₂ ∈ {2, 3, 4, 5}</text>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="81.59" y="-244.7" font-family="DejaVu Sans" font-size="10.00" fill="#1a1a2e">Constraint: x₁ + x₂ = 7</text>
|
||
|
|
</g>
|
||
|
|
<!-- prop -->
|
||
|
|
<g id="node2" class="node">
|
||
|
|
<title>prop</title>
|
||
|
|
<path fill="#ecfeff" stroke="#0891b2" stroke-width="2" d="M331.92,-191.56C331.92,-191.56 39,-191.56 39,-191.56 33,-191.56 27,-185.56 27,-179.56 27,-179.56 27,-129.28 27,-129.28 27,-123.28 33,-117.28 39,-117.28 39,-117.28 331.92,-117.28 331.92,-117.28 337.92,-117.28 343.92,-123.28 343.92,-129.28 343.92,-129.28 343.92,-179.56 343.92,-179.56 343.92,-185.56 337.92,-191.56 331.92,-191.56"/>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="39.96" y="-171.57" font-family="DejaVu Sans" font-weight="bold" font-size="13.00" fill="#0891b2">CONSTRAINT PROPAGATION  (Filterung)</text>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="39.96" y="-147.42" font-family="DejaVu Sans" font-size="10.00" fill="#1a1a2e">• x₁ = 1 ⇒ x₂ = 6  (nicht in Domain!)</text>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="39.96" y="-137.42" font-family="DejaVu Sans" font-size="10.00" fill="#1a1a2e">  ⟶ entferne 1 aus Domain(x₁)</text>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="39.96" y="-127.42" font-family="DejaVu Sans" font-size="10.00" fill="#1a1a2e">• Reduziert: x₁ ∈ {2, 3, 4}, x₂ ∈ {3, 4, 5}</text>
|
||
|
|
</g>
|
||
|
|
<!-- store->prop -->
|
||
|
|
<g id="edge1" class="edge">
|
||
|
|
<title>store->prop</title>
|
||
|
|
<path fill="none" stroke="#334155" stroke-width="2" d="M185.46,-233.8C185.46,-224.58 185.46,-214.29 185.46,-204.28"/>
|
||
|
|
<polygon fill="#334155" stroke="#334155" stroke-width="2" points="188.61,-204.33 185.46,-195.33 182.31,-204.33 188.61,-204.33"/>
|
||
|
|
</g>
|
||
|
|
<!-- sat -->
|
||
|
|
<g id="node3" class="node">
|
||
|
|
<title>sat</title>
|
||
|
|
<path fill="#f5f3ff" stroke="#7c3aed" stroke-width="2" d="M358.92,-74.28C358.92,-74.28 12,-74.28 12,-74.28 6,-74.28 0,-68.28 0,-62.28 0,-62.28 0,-12 0,-12 0,-6 6,0 12,0 12,0 358.92,0 358.92,0 364.92,0 370.92,-6 370.92,-12 370.92,-12 370.92,-62.28 370.92,-62.28 370.92,-68.28 364.92,-74.28 358.92,-74.28"/>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="12.96" y="-54.29" font-family="DejaVu Sans" font-weight="bold" font-size="13.00" fill="#7c3aed">SAT-SEARCH & CONFLICT LEARNING  (Nogoods)</text>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="12.96" y="-30.14" font-family="DejaVu Sans" font-size="10.00" fill="#1a1a2e">• Bei Widerspruch lernt der SAT-Core eine Klausel</text>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="12.96" y="-20.14" font-family="DejaVu Sans" font-size="10.00" fill="#1a1a2e">  („diese Belegung nie wieder prüfen“)</text>
|
||
|
|
<text xml:space="preserve" text-anchor="start" x="12.96" y="-10.14" font-family="DejaVu Sans" font-size="10.00" fill="#1a1a2e">• Non-chronological Backtracking</text>
|
||
|
|
</g>
|
||
|
|
<!-- prop->sat -->
|
||
|
|
<g id="edge2" class="edge">
|
||
|
|
<title>prop->sat</title>
|
||
|
|
<path fill="none" stroke="#334155" stroke-width="2" d="M185.46,-116.31C185.46,-106.95 185.46,-96.76 185.46,-86.92"/>
|
||
|
|
<polygon fill="#334155" stroke="#334155" stroke-width="2" points="188.61,-87.21 185.46,-78.21 182.31,-87.21 188.61,-87.21"/>
|
||
|
|
</g>
|
||
|
|
</g>
|
||
|
|
</svg>
|