notxia/unibo-ai-notes
1
0
Fork 0
mirror of https://github.com/NotXia/unibo-ai-notes.git synced 2025-12-16 19:32:21 +01:00
Code Issues Packages Projects Releases Wiki Activity

Moved CDMO1 in year1

Browse Source
This commit is contained in:
Tian Cheng (Riccardo) Xia
2024-04-11 21:23:48 +02:00
parent eed1920461
commit ea45a504cf
12 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
src/year1/combinatorial-decision-making-and-optimization/module1/ainotes.cls Symbolic link
View File

@ -0,0 +1 @@
../../../ainotes.cls

14
src/year1/combinatorial-decision-making-and-optimization/module1/cdmo1.tex Normal file
View File

@ -0,0 +1,14 @@
\documentclass[11pt]{ainotes}
\title{Combinatorial Decision Making\\and Optimization\\(Module 1)}
\date{2023 -- 2024}
\def\lastupdate{{PLACEHOLDER-LAST-UPDATE}}
\begin{document}
\makenotesfront
\input{./sections/_constraint_programming.tex}
\input{./sections/_sat.tex}
\eoc
\end{document}

BIN
src/year1/combinatorial-decision-making-and-optimization/module1/img/_cdcl_1uip.pdf Normal file
View File

Binary file not shown.

BIN
src/year1/combinatorial-decision-making-and-optimization/module1/img/_cdcl_cut.pdf Normal file
View File

Binary file not shown.

BIN
src/year1/combinatorial-decision-making-and-optimization/module1/img/_cdcl_example1.pdf Normal file
View File

Binary file not shown.

BIN
src/year1/combinatorial-decision-making-and-optimization/module1/img/_cdcl_example2.pdf Normal file
View File

Binary file not shown.

BIN
src/year1/combinatorial-decision-making-and-optimization/module1/img/_cdcl_example3.pdf Normal file
View File

Binary file not shown.

BIN
src/year1/combinatorial-decision-making-and-optimization/module1/img/_cdcl_example4.pdf Normal file
View File

Binary file not shown.

701
src/year1/combinatorial-decision-making-and-optimization/module1/img/cdcl_example.drawio Normal file
View File

@ -0,0 +1,701 @@
<mxfile host="Electron" modified="2024-03-15T16:02:44.844Z" agent="Mozilla/5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/23.1.5 Chrome/120.0.6099.109 Electron/28.1.0 Safari/537.36" etag="xqsC8_HsGit7oY8XCL57" version="23.1.5" type="device">
<diagram name="Pagina-1" id="TPm98Ap4iW5uKvmGSb2f">
<mxGraphModel dx="1103" dy="1812" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="827" pageHeight="1169" math="0" shadow="0">
<root>
<mxCell id="0" />
<mxCell id="1" parent="0" />
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-1" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;4&lt;/sub&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;3&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;6&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;sub&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="150" y="220" width="200" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-4" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;¬x&lt;sub&gt;1&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;4&lt;/sub&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;¬x&lt;sub&gt;1&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;3&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;6&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;sub&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;x&lt;sub&gt;7&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="60" y="-90" width="230" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-5" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="570" y="210" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-6" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="250" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-7" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="360" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-8" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;4&lt;/sub&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;3&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;6&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;sub&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;6&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="150" y="480" width="200" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-9" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="570" y="470" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-10" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="510" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-11" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="620" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-14" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="500" y="530" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-15" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="500" y="610" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-16" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-10" target="mCqeTS5OQJ7wAlwwDYhK-14">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="440" y="610" as="sourcePoint" />
<mxPoint x="490" y="560" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-20" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-16">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-17" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-11" target="mCqeTS5OQJ7wAlwwDYhK-15">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="546" as="sourcePoint" />
<mxPoint x="530" y="565" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-19" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-17">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-21" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-11" target="mCqeTS5OQJ7wAlwwDYhK-14">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="546" as="sourcePoint" />
<mxPoint x="530" y="565" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-22" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-21">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-36" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;&lt;font color=&quot;#009900&quot;&gt;x&lt;sub&gt;2&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;3&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;3&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;4&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;6&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;sub&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;6&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="150" y="760" width="200" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-37" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="570" y="750" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-38" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="790" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-39" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="400" y="900" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-40" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="500" y="810" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-41" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="500" y="890" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-42" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-38" target="mCqeTS5OQJ7wAlwwDYhK-40">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="440" y="890" as="sourcePoint" />
<mxPoint x="490" y="840" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-43" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-42">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-44" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-39" target="mCqeTS5OQJ7wAlwwDYhK-41">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="826" as="sourcePoint" />
<mxPoint x="530" y="845" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-45" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-44">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-46" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-39" target="mCqeTS5OQJ7wAlwwDYhK-40">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="826" as="sourcePoint" />
<mxPoint x="530" y="845" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-47" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-46">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-48" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="590" y="850" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-49" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-40" target="mCqeTS5OQJ7wAlwwDYhK-48">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="470" y="826" as="sourcePoint" />
<mxPoint x="510" y="835" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-50" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-49">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-51" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-41" target="mCqeTS5OQJ7wAlwwDYhK-48">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="570" y="846" as="sourcePoint" />
<mxPoint x="610" y="864" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-52" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-51">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-53" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;2&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="680" y="810" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-54" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="680" y="890" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-55" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-48" target="mCqeTS5OQJ7wAlwwDYhK-53">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="570" y="846" as="sourcePoint" />
<mxPoint x="610" y="864" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-56" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-55">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-10" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-57" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-48" target="mCqeTS5OQJ7wAlwwDYhK-54">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="660" y="864" as="sourcePoint" />
<mxPoint x="700" y="846" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-58" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;3&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-57">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-3" y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-59" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0.106;entryY=0.126;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-37" target="mCqeTS5OQJ7wAlwwDYhK-53">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="660" y="864" as="sourcePoint" />
<mxPoint x="700" y="846" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-60" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-59">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-61" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;&lt;font color=&quot;#009900&quot;&gt;x&lt;sub&gt;2&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;1&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;3&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;3&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;4&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;6&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;sub&gt;5&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;&lt;font color=&quot;#009900&quot;&gt;¬x&lt;/font&gt;&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;&lt;font color=&quot;#009900&quot;&gt;6&lt;/font&gt;&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;&lt;font color=&quot;#cccccc&quot;&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/font&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;&lt;font color=&quot;#cccccc&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/font&gt;&lt;/i&gt;&lt;/font&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="160" y="1020" width="200" height="180" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-62" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="580" y="1010" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-63" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="410" y="1050" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-64" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="410" y="1160" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-65" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="510" y="1070" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-66" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="510" y="1150" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-67" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-63" target="mCqeTS5OQJ7wAlwwDYhK-65">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="450" y="1150" as="sourcePoint" />
<mxPoint x="500" y="1100" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-68" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-67">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-69" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-64" target="mCqeTS5OQJ7wAlwwDYhK-66">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="480" y="1086" as="sourcePoint" />
<mxPoint x="540" y="1105" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-70" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-69">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-71" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-64" target="mCqeTS5OQJ7wAlwwDYhK-65">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="480" y="1086" as="sourcePoint" />
<mxPoint x="540" y="1105" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-72" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-71">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-73" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="600" y="1110" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-74" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-65" target="mCqeTS5OQJ7wAlwwDYhK-73">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="480" y="1086" as="sourcePoint" />
<mxPoint x="520" y="1095" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-75" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-74">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-76" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-66" target="mCqeTS5OQJ7wAlwwDYhK-73">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="580" y="1106" as="sourcePoint" />
<mxPoint x="620" y="1124" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-77" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-76">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-78" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;2&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="690" y="1070" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-79" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font style=&quot;border-color: var(--border-color); font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;3&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="690" y="1150" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-80" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-73" target="mCqeTS5OQJ7wAlwwDYhK-78">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="580" y="1106" as="sourcePoint" />
<mxPoint x="620" y="1124" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-81" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-80">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-10" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-82" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-73" target="mCqeTS5OQJ7wAlwwDYhK-79">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="670" y="1124" as="sourcePoint" />
<mxPoint x="710" y="1106" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-83" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;3&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-82">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-3" y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-84" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0.106;entryY=0.126;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-62" target="mCqeTS5OQJ7wAlwwDYhK-78">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="670" y="1124" as="sourcePoint" />
<mxPoint x="710" y="1106" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-85" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-84">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-88" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;κ&lt;/i&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#FFCCCC;verticalAlign=middle;labelPosition=center;verticalLabelPosition=middle;align=center;" vertex="1" parent="1">
<mxGeometry x="790" y="1110" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-89" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-78" target="mCqeTS5OQJ7wAlwwDYhK-88">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="790" y="1040" as="sourcePoint" />
<mxPoint x="847" y="1078" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-90" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-89">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-91" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-79" target="mCqeTS5OQJ7wAlwwDYhK-88">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="760" y="1106" as="sourcePoint" />
<mxPoint x="810" y="1124" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-92" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-91">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-93" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0.5;entryY=0;entryDx=0;entryDy=0;curved=1;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-62" target="mCqeTS5OQJ7wAlwwDYhK-88">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="760" y="1106" as="sourcePoint" />
<mxPoint x="810" y="1124" as="targetPoint" />
<Array as="points">
<mxPoint x="770" y="1020" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-94" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-93">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="1" y="9" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-96" value="&lt;font color=&quot;#ffffff&quot;&gt;Text&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="840" y="790" width="20" height="80" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-97" value="&lt;font color=&quot;#ffffff&quot;&gt;Text&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="840" y="510" width="20" height="80" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-98" value="&lt;font color=&quot;#ffffff&quot;&gt;Text&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="840" y="290" width="20" height="80" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-99" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="500" y="1370" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-100" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="330" y="1410" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-101" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="330" y="1520" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-102" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="430" y="1430" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-103" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="430" y="1510" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-104" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-100" target="mCqeTS5OQJ7wAlwwDYhK-102">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="370" y="1510" as="sourcePoint" />
<mxPoint x="420" y="1460" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-105" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-104">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-106" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-101" target="mCqeTS5OQJ7wAlwwDYhK-103">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="400" y="1446" as="sourcePoint" />
<mxPoint x="460" y="1465" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-107" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-106">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-108" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-101" target="mCqeTS5OQJ7wAlwwDYhK-102">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="400" y="1446" as="sourcePoint" />
<mxPoint x="460" y="1465" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-109" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-108">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-110" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="520" y="1470" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-111" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-102" target="mCqeTS5OQJ7wAlwwDYhK-110">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="400" y="1446" as="sourcePoint" />
<mxPoint x="440" y="1455" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-112" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-111">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-113" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-103" target="mCqeTS5OQJ7wAlwwDYhK-110">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="500" y="1466" as="sourcePoint" />
<mxPoint x="540" y="1484" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-114" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-113">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-115" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;2&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="610" y="1430" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-116" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font style=&quot;border-color: var(--border-color); font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;3&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="610" y="1510" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-117" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-110" target="mCqeTS5OQJ7wAlwwDYhK-115">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="500" y="1466" as="sourcePoint" />
<mxPoint x="540" y="1484" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-118" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-117">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-10" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-119" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-110" target="mCqeTS5OQJ7wAlwwDYhK-116">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="590" y="1484" as="sourcePoint" />
<mxPoint x="630" y="1466" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-120" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;3&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-119">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-3" y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-121" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0.106;entryY=0.126;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-99" target="mCqeTS5OQJ7wAlwwDYhK-115">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="590" y="1484" as="sourcePoint" />
<mxPoint x="630" y="1466" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-122" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-121">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-123" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;κ&lt;/i&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#FFCCCC;verticalAlign=middle;labelPosition=center;verticalLabelPosition=middle;align=center;" vertex="1" parent="1">
<mxGeometry x="710" y="1470" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-124" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-115" target="mCqeTS5OQJ7wAlwwDYhK-123">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="710" y="1400" as="sourcePoint" />
<mxPoint x="767" y="1438" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-125" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-124">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-126" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-116" target="mCqeTS5OQJ7wAlwwDYhK-123">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="680" y="1466" as="sourcePoint" />
<mxPoint x="730" y="1484" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-127" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-126">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-128" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0.5;entryY=0;entryDx=0;entryDy=0;curved=1;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-99" target="mCqeTS5OQJ7wAlwwDYhK-123">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="680" y="1466" as="sourcePoint" />
<mxPoint x="730" y="1484" as="targetPoint" />
<Array as="points">
<mxPoint x="690" y="1380" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-129" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-128">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="1" y="9" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-131" value="" style="endArrow=none;dashed=1;html=1;rounded=0;curved=1;strokeColor=#3399FF;strokeWidth=2;entryX=0.75;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" target="mCqeTS5OQJ7wAlwwDYhK-133">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="420" y="1560" as="sourcePoint" />
<mxPoint x="590" y="1350" as="targetPoint" />
<Array as="points">
<mxPoint x="380" y="1360" />
<mxPoint x="600" y="1470" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-133" value="&lt;font color=&quot;#3399ff&quot;&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub&gt;1&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt; x&lt;sub&gt;7&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;&amp;nbsp;&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub&gt;8&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="500" y="1320" width="130" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-135" value="" style="endArrow=none;dashed=1;html=1;rounded=0;strokeWidth=2;curved=1;strokeColor=#CC0000;entryX=0.25;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" target="mCqeTS5OQJ7wAlwwDYhK-137">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="610" y="1560" as="sourcePoint" />
<mxPoint x="670" y="1360" as="targetPoint" />
<Array as="points">
<mxPoint x="590" y="1450" />
<mxPoint x="620" y="1400" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-137" value="&lt;font color=&quot;#cc0000&quot;&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub style=&quot;&quot;&gt;1&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt; &lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub style=&quot;&quot;&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="640" y="1340" width="130" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-138" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;1&lt;/sub&gt;@1&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="660" y="1700" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-139" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;8&lt;/sub&gt;@2&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="490" y="1740" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-140" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;7&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#D5E8D4;" vertex="1" parent="1">
<mxGeometry x="490" y="1850" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-141" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="590" y="1760" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-142" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="590" y="1840" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-143" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-139" target="mCqeTS5OQJ7wAlwwDYhK-141">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="530" y="1840" as="sourcePoint" />
<mxPoint x="580" y="1790" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-144" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-143">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-145" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-140" target="mCqeTS5OQJ7wAlwwDYhK-142">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="560" y="1776" as="sourcePoint" />
<mxPoint x="620" y="1795" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-146" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;5&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-145">
<mxGeometry x="0.035" y="-2" relative="1" as="geometry">
<mxPoint y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-147" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-140" target="mCqeTS5OQJ7wAlwwDYhK-141">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="560" y="1776" as="sourcePoint" />
<mxPoint x="620" y="1795" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-148" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;6&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-147">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-11" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-149" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="680" y="1800" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-150" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-141" target="mCqeTS5OQJ7wAlwwDYhK-149">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="560" y="1776" as="sourcePoint" />
<mxPoint x="600" y="1785" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-151" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-150">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-152" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-142" target="mCqeTS5OQJ7wAlwwDYhK-149">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="660" y="1796" as="sourcePoint" />
<mxPoint x="700" y="1814" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-153" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;4&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-152">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="2" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-154" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;2&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="770" y="1760" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-155" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬&lt;/i&gt;&lt;font style=&quot;border-color: var(--border-color); font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i style=&quot;border-color: var(--border-color);&quot;&gt;x&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-style: italic;&quot;&gt;3&lt;/sub&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=none;" vertex="1" parent="1">
<mxGeometry x="770" y="1840" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-156" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-149" target="mCqeTS5OQJ7wAlwwDYhK-154">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="660" y="1796" as="sourcePoint" />
<mxPoint x="700" y="1814" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-157" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-156">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-10" y="-14" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-158" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-149" target="mCqeTS5OQJ7wAlwwDYhK-155">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="750" y="1814" as="sourcePoint" />
<mxPoint x="790" y="1796" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-159" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;3&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-158">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="-3" y="3" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-160" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0.106;entryY=0.126;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-138" target="mCqeTS5OQJ7wAlwwDYhK-154">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="750" y="1814" as="sourcePoint" />
<mxPoint x="790" y="1796" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-161" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;sub style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left; font-style: italic;&quot;&gt;1&lt;/sub&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-160">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-162" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 20px;&quot;&gt;&lt;i&gt;κ&lt;/i&gt;@3&lt;/font&gt;" style="ellipse;whiteSpace=wrap;html=1;fillColor=#FFCCCC;verticalAlign=middle;labelPosition=center;verticalLabelPosition=middle;align=center;" vertex="1" parent="1">
<mxGeometry x="870" y="1800" width="70" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-163" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-154" target="mCqeTS5OQJ7wAlwwDYhK-162">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="870" y="1730" as="sourcePoint" />
<mxPoint x="927" y="1768" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-164" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-163">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="-11" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-165" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0;exitDx=0;exitDy=0;entryX=0;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-155" target="mCqeTS5OQJ7wAlwwDYhK-162">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="840" y="1796" as="sourcePoint" />
<mxPoint x="890" y="1814" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-166" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-165">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="5" y="4" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-167" value="" style="endArrow=classic;html=1;rounded=0;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0.5;entryY=0;entryDx=0;entryDy=0;curved=1;" edge="1" parent="1" source="mCqeTS5OQJ7wAlwwDYhK-138" target="mCqeTS5OQJ7wAlwwDYhK-162">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="840" y="1796" as="sourcePoint" />
<mxPoint x="890" y="1814" as="targetPoint" />
<Array as="points">
<mxPoint x="850" y="1710" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-168" value="&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; text-align: left;&quot;&gt;&lt;font size=&quot;1&quot;&gt;2&lt;/font&gt;&lt;/i&gt;" style="edgeLabel;html=1;align=center;verticalAlign=middle;resizable=0;points=[];labelBackgroundColor=none;" vertex="1" connectable="0" parent="mCqeTS5OQJ7wAlwwDYhK-167">
<mxGeometry x="-0.0329" y="-1" relative="1" as="geometry">
<mxPoint x="1" y="9" as="offset" />
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-171" value="" style="endArrow=none;dashed=1;html=1;rounded=0;strokeWidth=2;curved=1;strokeColor=#CC0000;entryX=0.25;entryY=1;entryDx=0;entryDy=0;" edge="1" parent="1" target="mCqeTS5OQJ7wAlwwDYhK-172">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="770" y="1890" as="sourcePoint" />
<mxPoint x="830" y="1690" as="targetPoint" />
<Array as="points">
<mxPoint x="750" y="1780" />
<mxPoint x="780" y="1730" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-172" value="&lt;font color=&quot;#cc0000&quot;&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub style=&quot;&quot;&gt;1&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt; &lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px; text-align: left;&quot;&gt;¬x&lt;sub style=&quot;&quot;&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="800" y="1670" width="130" height="30" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-173" value="&lt;font style=&quot;font-size: 20px;&quot; face=&quot;Computer modern&quot;&gt;&lt;i&gt;c&lt;sub style=&quot;&quot;&gt;1&lt;/sub&gt;:&amp;nbsp;¬x&lt;sub&gt;1&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨ &lt;i&gt;x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub&gt;4&lt;/sub&gt;&amp;nbsp;&lt;br&gt;c&lt;sub&gt;2&lt;/sub&gt;:&amp;nbsp;¬x&lt;sub&gt;1&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;2&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;3&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;3&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;¬x&lt;sub&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;4&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub style=&quot;&quot;&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;x&lt;sub&gt;6&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;5&lt;/sub&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;sub&gt;5&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;x&lt;sub&gt;7&lt;/sub&gt;&lt;/i&gt;&lt;br&gt;&lt;i&gt;c&lt;/i&gt;&lt;span style=&quot;font-style: italic;&quot;&gt;&lt;sub&gt;6&lt;/sub&gt;&lt;/span&gt;&lt;i&gt;:&amp;nbsp;¬x&lt;/i&gt;&lt;sub style=&quot;font-style: italic;&quot;&gt;6&lt;/sub&gt;&lt;i&gt;&amp;nbsp;&lt;/i&gt;∨&amp;nbsp;&lt;i&gt;x&lt;sub&gt;7&lt;/sub&gt;&amp;nbsp;&lt;/i&gt;∨&lt;i&gt;&amp;nbsp;¬x&lt;sub style=&quot;&quot;&gt;8&lt;br&gt;&lt;/sub&gt;&lt;/i&gt;&lt;/font&gt;&lt;b&gt;&lt;u&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;c&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;:&amp;nbsp;&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;¬x&lt;sub style=&quot;border-color: var(--border-color);&quot;&gt;1&amp;nbsp;&lt;/sub&gt;&lt;/i&gt;&lt;span style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;∨&lt;/span&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;&amp;nbsp;&lt;/i&gt;&lt;i style=&quot;border-color: var(--border-color); font-family: &amp;quot;Computer modern&amp;quot;; font-size: 20px;&quot;&gt;¬x&lt;sub style=&quot;border-color: var(--border-color);&quot;&gt;4&lt;/sub&gt;&lt;/i&gt;&lt;/u&gt;&lt;/b&gt;&lt;font face=&quot;Computer modern&quot;&gt;&lt;br&gt;&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="260" y="1680" width="200" height="210" as="geometry" />
</mxCell>
<mxCell id="mCqeTS5OQJ7wAlwwDYhK-174" value="&lt;font face=&quot;Computer modern&quot; style=&quot;font-size: 18px;&quot;&gt;(1UIP)&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="685" y="1830" width="60" height="30" as="geometry" />
</mxCell>
</root>
</mxGraphModel>
</diagram>
</mxfile>

484
src/year1/combinatorial-decision-making-and-optimization/module1/sections/_constraint_programming.tex Normal file
View File

@ -0,0 +1,484 @@
\chapter{Constraint programming}
\section{Definitions}
\begin{description}
\item[Constraint satisfaction problem (CSP)] \marginnote{Constraint satisfaction problem (CSP)}
Triple $\langle X, D, C \rangle$ where:
\begin{itemize}
\item $X$ is the set of decision variables $\{ x_1, \dots, x_n \}$.
\item $D$ is the set of domains $\{ D(X_1), \dots, D(X_n) \}$ or $\{ D_1, \dots, D_n \}$ for $X$.
\item $C$ is the set of constraints $\{ C_1, \dots, C_m \}$.
Each $C_i$ is a relation over the domain of $X$ (i.e. $C_i \subseteq D_j \times \dots \times D_k$).
\end{itemize}
\item[Constraint optimization problem (COP)] \marginnote{Constraint optimization problem (COP)}
Tuple $\langle X, D, C, f \rangle$ where $\langle X, D, C \rangle$ is a CSP and
$f$ is the objective variable to minimize or maximize.
\item[Constraint] \marginnote{Constraint}
\phantom{}
\begin{description}
\item[Extensional representation] List all allowed combinations.
\item[Intensional representation] Declarative relations between variables.
\end{description}
\item[Symmetry] \marginnote{}
Search states that lead to the same result.
\begin{description}
\item[Variable symmetry] \marginnote{Variable symmetry}
A permutation of the assignment order of the variables results in the same feasible or unfeasible solution.
\item[Value symmetry] \marginnote{Value symmetry}
A permutation of the values in the domain results in the same feasible or unfeasible solution.
\end{description}
\begin{remark}
Variable and value symmetries can be combined resulting in a total of $2n!$ possible symmetries.
\end{remark}
\end{description}
\section{Modeling techniques}
\begin{description}
\item[Auxiliary variables] \marginnote{Auxiliary variables}
Add new variables to capture constraints difficult to model or
to reduce the search space by collapsing multiple variables into one.
\item[Global constraints] \marginnote{Global constraints}
Relation between an arbitrary number of variables.
It is usually computationally faster than listing multiple constraints.
\item[Implied constraints] \marginnote{Implied constraints}
Semantically redundant constraints with the advantage of pruning the search space earlier.
\begin{remark}
A purely redundant constraint is also an implied constraint but it does not give any computational improvement.
\end{remark}
\item[Symmetry breaking constraints] \marginnote{Symmetry breaking constraints}
Constraints to avoid considering symmetric states.
Usually, it is sufficient to fix an ordering of the variables.
\begin{remark}
When introducing symmetry breaking constraints,
it might be possible to add new simplifications and implied constraints.
\end{remark}
\item[Dual viewpoint] \marginnote{Dual viewpoint}
Modeling a problem from a different perspective might result in a more efficient search.
\begin{example}
Exploiting geometric symmetries.
\end{example}
\item[Combined model] \marginnote{Combined model}
Merging two or more models of the same problem by adding channeling constraints to guarantee consistency.
Combining two models can be useful for obtaining the advantages of both
(e.g. one model uses global constraints, while the other handles symmetries).
\begin{remark}
When combining multiple models, some constraints might be simplified as one of the models already captures it natively.
\end{remark}
\end{description}
\section{Constraints}
\subsection{Local consistency}
Examine individual constraints and detect inconsistent partial assignments.
\begin{description}
\item[Generalized arc consistency (GAC)] \marginnote{Generalized arc consistency (GAC)}
\phantom{}
\begin{description}
\item[Support]
Given a constraint defined on $k$ variables $C \subseteq D(X_1)\times \dots \times D(X_k)$,
each tuple $(d_1, \dots, d_k) \in C$ (i.e. allowed variables assignment) is a support for $C$.
\end{description}
A constraint $C(X_1, \dots, X_k)$ is GAC (GAC($C$)) iff:
\[ \forall X_i \in \{ X_1, \dots, X_k \}, \forall v \in D(X_i): \text{$v$ belongs to a support for $C$} \]
\begin{remark}
A CSP is GAC when all its constraints are GAC.
\end{remark}
\begin{example}[Generalized arc consistency]
Given the variables $D(X_1) = \{ 1, 2, 3 \}$, $D(X_2) = \{ 1, 2 \}$, $D(X_3) = \{ 1, 2 \}$ and
the constraint $C: \texttt{alldifferent}([X_1, X_2, X_3])$,
$C$ is not GAC as $1 \in D(X_1)$ and $2 \in D(X_2)$ do not have a support.
By applying a constraint propagation algorithm, we can reduce the domain to:
$D(X_1) = \{ \cancel{1}, \cancel{2}, 3 \}$ and $D(X_2) = D(X_3) = \{ 1, 2 \}$.
Now $C$ is GAC.
\end{example}
\begin{description}
\item[Arc consistency (AC)] \marginnote{Arc consistency (AC)}
A constraint is arc consistent when its binary constrains are GAC.
\begin{example}[Arc consistency]
Given the variables $D(X_1) = \{ 1, 2, 3 \}$, $D(X_2) = \{ 2, 3, 4 \}$ and the constraint $C: X_1 = X_2$,
$C$ is not arc consistent as $1 \in D(X_1)$ and $4 \in D(X_2)$ do not have a support.
By applying a constraint propagation algorithm, we can reduce the domain to:
$D(X_1) = \{ \cancel{1}, 2, 3 \}$ and $D(X_2) = \{ 2, 3, \cancel{4} \}$.
Now $C$ is arc consistent.
\end{example}
\end{description}
\item[Bounds consistency (BC)] \marginnote{Bounds consistency (BC)}
Can be applied on totally ordered domains.
The domain of a variable $X_i$ is relaxed from $D(X_i)$ to the interval $[\min\{D(X_i)\}, \max\{D(X_i)\}]$.
\begin{description}
\item[Bound support]
Given a constraint defined on $k$ variables $C(X_1, \dots, X_k)$,
each tuple $(d_1, \dots, d_k) \in C$, where $d_i \in [\min\{D(X_i)\}, \max\{D(X_i)\}]$, is a bound support for $C$.
\end{description}
A constraint $C(X_1, \dots, X_k)$ is BC (BC($C$)) iff:
\[
\begin{split}
\forall X_i &\in \{ X_1, \dots, X_k \}: \\
&\text{$\min\{D(X_i)\}$ and $\max\{D(X_i)\}$ belong to a bound support for $C$}
\end{split}
\]
\begin{remark}
BC might not detect all GAC inconsistencies, but it is computationally cheaper.
\end{remark}
\begin{remark}
On monotonic constraints, BC and GAC are equivalent.
\end{remark}
\begin{example}
Given the variables $D(X_1) = D(X_2) = D(X_3) = \{ 1, 3 \}$ and the constraint $C: \texttt{alldifferent}([X_1, X_2, X_3])$,
$C$ is BC as all $\min\{D(X_i)\}$ and $\max\{D(X_i)\}$ belong to the bound support $\{ (d_1, d_2, d_3) \mid d_i \in [1, 3] \land d_1 \neq d_2 \neq d_3 \}$
On the other hand, $C$ fails with GAC.
\end{example}
\end{description}
\subsection{Constraint propagation}
\begin{description}
\item[Constraint propagation] \marginnote{Constraint propagation}
Algorithm that removes values from the domains of the variables to achieve a given level of consistency.
Constraint propagation algorithms interact with each other and already propagated constraints might be woke up again by another constraint.
Propagation will eventually reach a fixed point.
\item[Specialized propagation] \marginnote{Specialized propagation}
Propagation algorithm specific to a given constraint.
Allows to exploit the semantics of the constraint for a generally more efficient approach.
\end{description}
\subsection{Global constraints}
Constraints to capture complex, non-binary, and recurring features of the variables.
Usually, global constraints are enforced using specialized propagation algorithms.
\subsubsection{Counting constraints}
\marginnote{Counting constraints}
Constrains the number of variables satisfying a condition
or the occurrences of certain values.
\begin{descriptionlist}
\item[All-different]
Enforces that all variables assume a different value.
\[ \texttt{alldifferent}([X_1, \dots, X_k]) \iff \forall i, j, \in \{ 1, \dots, k\}, i \neq j: X_i \neq X_j \]
\item[Global cardinality]
Enforces the number of times some values should appear among the variables.
\[
\begin{split}
\texttt{gcc}([X_1, \dots, X_k], &[v_1, \dots, v_m], [O_1, \dots, O_m]) \iff \\
& \forall j \in \{1, \dots, m\}: \left\vert \{ X_i \mid X_i = v_j \} \right\vert = O_j
\end{split}
\]
\item[Among]
Constrains the number of occurrences of certain values among the variables.
\[
\texttt{among}([X_1, \dots, X_k], \{v_1, \dots, v_n\}, l, u) \iff l \leq \left\vert \{ X_i \mid X_i \in \{v_1, \dots, v_n\} \} \right\vert \leq u
\]
\end{descriptionlist}
\subsubsection{Sequencing constraints}
\marginnote{Sequencing constraints}
Enforces a pattern on a sequence of variables.
\begin{descriptionlist}
\item[Sequence]
Enforces the number of times certain values can appear in a subsequence of a given length $q$.
\[
\begin{split}
\texttt{sequence}(l, u, q, &[X_1, \dots, X_k], \{v_1, \dots, v_n\}) \iff \\
& \forall i \in [1, \dots, k-q+1]: \texttt{among}([X_1, \dots, X_{i+q-1}], \{v_1, \dots, v_n\}, l, u)
\end{split}
\]
\end{descriptionlist}
\subsubsection{Scheduling constraints}
\marginnote{Scheduling constraints}
Useful to schedule tasks with release times, duration, deadlines, and resource limitations.
\begin{descriptionlist}
\item[Disjunctive resource]
Enforces that the tasks do not overlap over time.
Given the start time $S_i$ and the duration $D_i$ of $k$ tasks:
\[
\begin{split}
\texttt{disjunctive}([S_1, \dots, S_k], &[D_1, \dots, D_k]) \iff \\
& \forall i < j: (S_i + D_i \leq S_j) \vee (S_j + D_j \leq S_i)
\end{split}
\]
\item[Cumulative resource]
Constrains the usage of a shared resource.
Given a resource with capacity $C$ and the start time $S_i$, the duration $D_i$, and the resource requirement $R_i$ of $k$ tasks:
\[
\begin{split}
\texttt{cumulative}([S_1, \dots, S_k], &[D_1, \dots, D_k], [R_1, \dots, R_k], C) \iff \\
& \forall u \in \{ D_1, \dots, D_k \}: \sum_{\text{$i$ s.t. $S_i \leq u < S_i+D_i$}} R_i \leq C
\end{split}
\]
\end{descriptionlist}
\subsubsection{Ordering constraints}
\marginnote{Ordering constraints}
Enforce an ordering between variables or values.
\begin{descriptionlist}
\item[Lexicographic ordering]
Enforces that a sequence of variables is lexicographically less than or equal to another sequence.
\[
\begin{split}
\texttt{lex$\leq$}([X_1, \dots, X_k], [Y_1, \dots, Y_k]) \iff & X_1 \leq Y_1 \land \\
&(X_1 = Y_1 \Rightarrow X_2 \leq Y_2) \land \\
& \dots \land \\
&((X_1 = Y_1 \land \dots \land X_{k-1} = Y_{k-1}) \Rightarrow X_k \leq Y_k)
\end{split}
\]
\end{descriptionlist}
\subsubsection{Generic purpose constraints}
\marginnote{Generic purpose constraints}
Define constraints in an extensive way.
\begin{descriptionlist}
\item[Table]
Associate to the variables their allowed assignments.
\end{descriptionlist}
\subsubsection{Specialized propagation}
\begin{descriptionlist}
\item[Constraint decomposition] \marginnote{Constraint decomposition}
A global constraint is decomposed into smaller and simpler constraints with known propagation algorithms.
\begin{remark}
As the problem is decomposed, some inconsistencies may not be detected.
\end{remark}
\begin{example}(Decomposition of \texttt{among})
The \texttt{among} constraint can be decomposed as follows:
\begin{descriptionlist}
\item[Variables]
$B_i$ with $D(B_i) = \{ 0, 1 \}$ for $1 \leq i \leq k$.
\item[Constraints] \phantom{}
\begin{itemize}
\item $C_i: B_i = 1 \iff X_i \in v$ for $1 \leq i \leq k$.
\item $C_{k+1}: \sum_{i} B_i = N$.
\end{itemize}
\end{descriptionlist}
AC($C_i$) and BC($C_{k+1}$) ensures GAC on \texttt{among}.
\end{example}
\item[Dedicated propagation algorithm] \marginnote{Dedicated propagation algorithm}
Ad-hoc algorithm that implements an efficient propagation.
\begin{example}(\texttt{alldifferent} through maximal matching)
\begin{descriptionlist}
\item[Bipartite graph]
Graph where the edges are partitioned in two groups $U$ and $V$.
Nodes in $U$ can only connect to nodes in $V$.
\item[Maximal matching]
Largest subsets of edges such that there are no edges with nodes in common.
\end{descriptionlist}
Define a bipartite graph $G=(U \cup V, E)$ where:
\begin{itemize}
\item $U = \{ X_1, \dots, X_k \}$ are the variables.
\item $V = D(X_1) \cup \dots \cup D(X_k)$ are the possible values of the variables.
\item $E = \{ (X_i, v) \mid X_i \in U, v \in V: v \in D(X_i) \}$
contains the edges that connect every variable in $U$ to its possible values in $V$.
\end{itemize}
All the possible variable assignments of $X_1, \dots, X_k$ are the maximal matchings in $G$.
\end{example}
\end{descriptionlist}
\section{Search}
\begin{description}
\item[Backtraking tree search] \marginnote{Backtraking tree search}
Tree where nodes are variables and branches are variable assignments.
\item[Systematic search] \marginnote{Systematic search}
Instantiate and explore the tree depth first.
Constraints are checked when all variables are assigned (i.e. when a leaf is reached)
and the search backtracks of one decision if it fails.
This approach has exponential complexity.
\item[Search and propagation] \marginnote{Search and propagation}
Propagate the constraints after an assignment to
remove inconsistent values from the domain of yet unassigned variables.
\end{description}
\subsection{Search heuristics}
\begin{descriptionlist}
\item[Static heuristic] \marginnote{Static heuristic}
The order of exploration of the variables is fixed before search.
\item[Dynamic heuristic] \marginnote{Dynamic heuristic}
The order of exploration of the variables is determined during search.
\end{descriptionlist}
\begin{description}
\item[Fail-first (FF)] \marginnote{Fail-first (FF)}
Try the variables that are most likely to fail in order to maximize propagation.
\begin{description}
\item[Minimum domain] \marginnote{Minimum domain}
Assign the variable with the minimum domain size.
\item[Most constrained] \marginnote{Most constrained}
Assign the variable with the maximum degree (i.e. number of constraints that involve it).
\item[Combination] \marginnote{Combination}
Combine both minimum domain and most constrained to minimize the value $\frac{\text{domain size}}{\text{degree}}$.
\item[Weighted degree] \marginnote{Weighted degree}
Each constraint $C$ starts with a weight $w(C) = 1$.
During propagation, when a constraint $C$ fails, its weight is increased by 1.
The weighted degree of a variable $X_i$ is:
\[ w(X_i) = \sum_{\text{$C$ s.t. $C$ involves $X_i$}} w(C) \]
Assign the variable with minimum $\frac{\vert D(X_i) \vert}{w(X_i)}$.
\end{description}
\item[Heavy tail behavior]
Instances of a problem that are particularly hard and expensive to solve.
\begin{description}
\item[Randomization] \marginnote{Randomization}
Sometimes, make a random choice:
\begin{itemize}
\item Randomly choose the variable or value to assign.
\item Break ties randomly.
\end{itemize}
\item[Restarting] \marginnote{Restarting}
Restart the search after a certain amount of resources (e.g. search steps) have been consumed.
The new search can exploit past knowledge, change heuristics, or use randomization.
\begin{description}
\item[Constant restart]
Restart after a fixed number $L$ of resources have been used.
\item[Geometric restart]
At each restart, the resource limit $L$ is multiplied by a factor $\alpha$.
This will result in a sequence $L, \alpha L, \alpha^2 L, \dots$.
\item[Luby restart]
\phantom{}
\begin{descriptionlist}
\item[Luby sequence]
The first element of the sequence is 1. Then, the sequence is iteratively computed as follows:
\begin{itemize}
\item Repeat the current sequence.
\item Add $2^{i+1}$ at the end of the sequence.
\end{itemize}
\begin{example}
$[1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, \dots]$
\end{example}
\end{descriptionlist}
At the $i$-th restart, the resource limit $L$ is multiplied by a factor determined by the $i$-th element of the Luby sequence.
\end{description}
\begin{remark}
Weighted degree and restarts work well together when weights are carried over.
\end{remark}
\begin{remark}
Restarting on deterministic heuristics does not give any advantage.
\end{remark}
\end{description}
\end{description}
\subsection{Constraint optimization problems}
\begin{description}
\item[Branch and bound] \marginnote{Branch and bound}
Solves a COP by solving a sequence of CSPs.
\begin{enumerate}
\item Find a feasible solution and add a bounding constraint
to enforce that future solutions are better than this one.
\item Backtrack the last decision and look for a new solution on the same tree with the new constraint.
\item Repeat until the problem becomes unfeasible. The last solution is optimal.
\end{enumerate}
\end{description}
\subsection{Large neighborhood search (LNS)}
\marginnote{Large neighborhood search (LNS)}
Hybrid between constraint programming and heuristic search.
\begin{enumerate}
\item Find an initial solution $s$ using CP.
\item Create a partial solution $N(s)$ by taking some assignments from the solution $s$ and leaving the other unassigned.
\item Explore the large neighborhood using CP starting from $N(s)$.
\end{enumerate}

482
src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex Normal file
View File

@ -0,0 +1,482 @@
\chapter{SAT solver}
\begin{description}
\item[Satifiability (SAT)] \marginnote{SAT}
Given a propositional formula $f$,
find an assignment of the variables to make the formula true.
If $f$ is satisfiable, we say that it is SAT. Otherwise, it is UNSAT.
\end{description}
\begin{theorem}(Cook-Levin) \marginnote{Cook-Levin theorem}
SAT is NP-complete.
\begin{descriptionlist}
\item[NP-complete]
A problem is NP-complete iff it is in NP and every NP problem can be reduced to it.
\begin{remark}
All problems in NP can be reduced to SAT.
\end{remark}
\end{descriptionlist}
\end{theorem}
\begin{description}
\item[Satisfiable formula] \marginnote{Satisfiable formula}
A formula $f$ is satisfiable iff there is an assignment of the variables that makes it true.
\item[Valid formula] \marginnote{Valid formula}
A formula $f$ is valid iff any assignment of the variables makes it true.
\begin{remark}
$f$ is valid iff $\lnot f$ is UNSAT.
\end{remark}
\item[SAT solver] \marginnote{SAT solver}
Given a problem, the following steps should be followed to solve it using a SAT solver:
\begin{enumerate}
\item Formalize the problem into a propositional formula.
\item Depending on the solver, it might be necessary to convert it into CNF.
\item Feed the formula to a SAT solver.
\item The result can be an assignment of the variables (SAT) or a failure (UNSAT).
\end{enumerate}
\end{description}
\section{Solvers}
\subsection{Resolution}
\begin{description}
\item[Resolution] \marginnote{Resolution}
Basic approach for SAT.
Prove that a set of CNF clauses is UNSAT by deriving new clauses until a contradiction is reached.
Resolution rules to derive new clauses are:
\begin{descriptionlist}
\item[Resolution rule] \marginnote{Resolution rule}
\phantom{}
\begin{minipage}{0.4\linewidth}
\begin{prooftree}
\AxiomC{$p \vee V$}
\AxiomC{$\lnot p \vee W$}
\BinaryInfC{$V \vee W$}
\end{prooftree}
\end{minipage}
\item[Unit resolution] \marginnote{Unit resolution}
\begin{minipage}{0.4\linewidth}
\begin{prooftree}
\AxiomC{$p$}
\AxiomC{$\lnot p \vee W$}
\BinaryInfC{$W$}
\end{prooftree}
\end{minipage}
\begin{minipage}{0.4\linewidth}
\begin{prooftree}
\AxiomC{$\lnot p$}
\AxiomC{$p \vee V$}
\BinaryInfC{$V$}
\end{prooftree}
\end{minipage}
Note that this is equivalent to the rule of implication elimination:\\
\begin{minipage}{0.4\linewidth}
\begin{prooftree}
\AxiomC{$p$}
\AxiomC{$p \Rightarrow W$}
\BinaryInfC{$W$}
\end{prooftree}
\end{minipage}
\begin{minipage}{0.4\linewidth}
\begin{prooftree}
\AxiomC{$\lnot p$}
\AxiomC{$\lnot p \Rightarrow V$}
\BinaryInfC{$V$}
\end{prooftree}
\end{minipage}
\end{descriptionlist}
\end{description}
\begin{example}
Given the CNF formula:
\[ (p \vee q) \land (\lnot r \vee s) \land (\lnot q \vee r) \land (\lnot r \vee \lnot s) \land (\lnot p \vee r) \]
Resolution can be applied as follows:
\begin{itemize}
\item The starting clauses are:
$(p \vee q) \cdot (\lnot r \vee s) \cdot (\lnot q \vee r) \cdot (\lnot r \vee \lnot s) \cdot (\lnot p \vee r)$
\item From $(p \vee q)$ and $(\lnot q \vee r)$, one can derive $(p \vee r)$.
\item From $(\lnot p \vee r)$ and $(p \vee r)$, one can derive $r$.
\item From $(\lnot r \vee s)$ and $r$, one can derive $s$.
\item From $(\lnot r \vee \lnot s)$ and $s$, one can derive $\lnot r$.
\item From $r$ and $\lnot r$, one reaches $\bot$.
\end{itemize}
\end{example}
\subsection{DPLL algorithm}
\begin{description}
\item[DPLL] \marginnote{DPLL}
Algorithm based on unit resolution.
Given a set of clauses, DPLL is applied as follows:
\begin{enumerate}
\item Apply unit resolution as long as possible
(i.e. for every clause containing a single literal $l$, remove $\lnot l$ from all clauses.
Clauses containing $l$ can also be removed as they are redundant).
\item Choose a variable $p$.
\item Recursively apply DPLL by assuming $p$ in one call and $\lnot p$ in another.
\end{enumerate}
\begin{theorem}
DPLL is complete.
\end{theorem}
\begin{remark}
DPLL efficiency strongly depends on the variables.
\end{remark}
\end{description}
\begin{example}
Given a CNF formula with clauses:
\[ (\lnot p \vee \lnot s) \cdot (\lnot p \vee \lnot r) \cdot (\lnot q \vee \lnot t) \cdot (p \vee r) \cdot (p \vee s) \cdot (r \vee t) \cdot (\lnot s \vee t) \cdot (q \vee s) \]
There are no unit clauses, so we choose the variable $p$ and consider the cases where $p$ and where $\lnot p$.
By assuming $p$, unit resolution can be applied as follows:
\begin{itemize}
\item $p$ with $(\lnot p \vee \lnot s)$ derives $\lnot s$.
\item $p$ with $(\lnot p \vee \lnot r)$ derives $\lnot r$.
\item $\lnot s$ with $(q \vee s)$ derives $q$.
\item $\lnot r$ with $(r \vee t)$ derives $t$.
\item $q$ with $(\lnot q \vee \lnot t)$ derives $\not t$.
\item $t$ and $\lnot t$ bring to $\bot$. This branch is UNSAT.
\end{itemize}
By assuming $\lnot p$, unit resolution can be applied as follows:
\begin{itemize}
\item $\lnot p$ with $(p \vee r)$ derives $r$.
\item $\lnot p$ with $(p \vee s)$ derives $s$.
\item $s$ with $(\lnot s \vee t)$ derives $t$.
\item $t$ with $(\lnot q \vee \lnot t)$ derives $\lnot q$.
\end{itemize}
We reached a full assignment $\langle \lnot p, r, s, t, \lnot q \rangle$. The formula is SAT.
\end{example}
\begin{description}
\item[DPLL implementation] \marginnote{DPLL algorithm}
An efficient implementation of DPLL uses a list $M$ of the literals that have been decided or derived.
\begin{description}
\item[Notations] \phantom{}
\begin{itemize}[leftmargin=*]
\item A literal $l$ holds in $M$ ($M \models l$) iff $l$ is in $M$.
\item $M$ contradicts a clause $C$ ($M \models \lnot C$) iff for every literal $l$ in $C$, $M \models \lnot l$.
\item A literal $l$ is undefined iff $M \cancel{\models} l$ and $M \cancel{\models} \lnot l$.
\item A decision literal (i.e. literal assumed to hold) is denoted as $l^\mathcal{D}$.
\end{itemize}
\end{description}
The algorithm follows four rules:
\begin{descriptionlist}
\item[\texttt{UnitPropagate}]
If the CNF contains a clause $(A \vee l)$ such that $M \models \lnot A$ and $l$ is an undefined literal,
then there is a transition:
\[ M \rightarrow Ml \]
\item[\texttt{Decide}]
When \texttt{UnitPropagate} it not possible, an undefined literal $l$ is assumed to hold (it becomes a decision literal):
\[ M \rightarrow Ml^\mathcal{D} \]
\item[\texttt{Backtrack}]
When a branch is UNSAT, the algorithm backtracks to the nearest decision literal and negates it.
Given a clause $C$ of the CNF, if $Ml^\mathcal{D}N \models \lnot C$ and $N$ does not contain other decision literals,
then there is a transition:
\[ Ml^\mathcal{D}N \rightarrow M \lnot l \]
\item[\texttt{Fail}]
Given a clause $C$ of the CNF, if $M \models \lnot C$ and $M$ contains a definitive assignment of all the variables (i.e. no decision literals),
then there is a transition:
\[ M \rightarrow \text{fail} \]
\end{descriptionlist}
In the end, if the formula is SAT, $M$ contains an assignment of the variables.
\end{description}
\begin{remark}
Compared to resolution, DPLL is more memory efficient.
\end{remark}
\subsection{Conflict-driven clause learning (CDCL)}
DPLL with two improvements:
\begin{descriptionlist}
\item[Clause learning]
When a contradiction is found, augment the original CNF with a conflict clause
to prune the search space.
The conflict clause is obtained through resolution by combining two clauses that cause the contradiction.
\item[\texttt{Backjumping}]
Depending on the type of contradiction, skip decision literals that are not causing the conflict
and directly backtrack to an earlier relevant decision literal.
Given a clause $C$ of the CNF, if $Ml^\mathcal{D}N \models \lnot C$ and
there is a clause $(C' \vee l')$ derivable from the CNF such that $M \models \lnot C'$ and
$l'$ is undefined, then there is a transition:
\[ Ml^\mathcal{D}N \rightarrow Ml' \]
Note that $N$ might contain other decision literals and $(C' \vee l')$ is a conflict clause.
\begin{remark}
\texttt{Backjumping} can be seen as \texttt{UnitPropagate} applied on conflict clauses.
\end{remark}
\end{descriptionlist}
\begin{description}
\item[Implication graph]
DAG $G=(V, E)$ to record the history of decisions and unit resolutions.
\begin{descriptionlist}
\item[Vertex] Can be:
\begin{itemize}
\item A decision or derived literal (denoted as $l@d$, where $l$ is the literal and $d$ the decision level it originated from).
\item A marker to indicate a conflict (denoted as $\kappa@d$, where $d$ is the decision level it originated from).
\end{itemize}
\item[Edge]
Has form $v \xrightarrow{c_i} w$ and indicates that $w$ is obtained using the clause $c_i$ and the literal $v$.
\end{descriptionlist}
\begin{example}
Starting from the clauses $c_1, \dots, c_6$ of a CNF, one can build the implication graph while running DPLL/CDCL.
In this example, the decision literals (green nodes) are assigned following this order: $x_1 \rightarrow x_8 \rightarrow \lnot x_7$:
\begin{center}
\includegraphics[width=0.8\linewidth]{./img/_cdcl_example1.pdf}
\end{center}
\[ M \rightarrow M x_1^\mathcal{D} x_8^\mathcal{D} \lnot x_7^\mathcal{D} \]
Then, it is possible to derive implied variables using unit resolution starting from the decision literals:
\begin{center}
\includegraphics[width=0.8\linewidth]{./img/_cdcl_example2.pdf}
\end{center}
\[ M \rightarrow M \lnot x_6 \lnot x_5 \]
And so on:
\begin{center}
\includegraphics[width=0.8\linewidth]{./img/_cdcl_example3.pdf}
\end{center}
\[ M \rightarrow M x_4 x_2 \lnot x_3 \]
As $c_2$ is UNSAT, we reached a contradiction:
\begin{center}
\includegraphics[width=0.8\linewidth]{./img/_cdcl_example4.pdf}
\end{center}
\end{example}
\begin{remark}
Any cut that separates sources (decision literals) and the sink (contradiction node) is a valid conflict clause for backjumping.
\begin{example} \phantom{}
\begin{center}
\includegraphics[width=0.55\linewidth]{./img/_cdcl_cut.pdf}
\end{center}
\end{example}
\end{remark}
\item[Unit implication point (UIP)]
Given an implication graph where the latest decision node is $(l@d)$ and the conflict node is $(\kappa@d)$,
a node is a unit implication point iff it appears in all the paths from $(l@d)$ to $(\kappa@d)$.
The UIP closest to the conflict is denoted as 1UIP.
\begin{remark}
The decision node $(l@d)$ itself is a UIP.
\end{remark}
\item[1UIP-based backjumping]
In case of conflict, use the conflict clause obtained by cutting in front of the 1UIP.
\begin{remark}
This allows to:
\begin{itemize}
\item Reduce the size of the conflict clause.
\item Guarantee the highest backtrack jump.
\end{itemize}
\end{remark}
\begin{example}
\phantom{}
\begin{center}
\includegraphics[width=0.75\linewidth]{./img/_cdcl_1uip.pdf}
\end{center}
By adding the conflict clause $(\lnot x_1 \vee \lnot x_4)$, we can backjump up to $x_8^\mathcal{D}$
(not to $x_1^\mathcal{D}$ as it makes the conflict clause a unit).
\[ x_1^\mathcal{D} x_8^\mathcal{D} \lnot x_7^\mathcal{D} \lnot x_6 \lnot x_5 x_4 x_2 \lnot x_3 \rightarrow x_1^\mathcal{D} \lnot x_4\]
\end{example}
\end{description}
\section{Encodings}
\begin{description}
\item[Cardinality constraints] \marginnote{Cardinality constraints}
Constraints of the form:
\[ \sum_{1 \leq i \leq n} x_i \bowtie k \]
where $k \in \mathbb{N}$ and $\bowtie\,\, \in \{ <, \leq, =, \neq, \geq, > \}$.
\item[$\mathbf{k=1}$ constraints] \marginnote{$k=1$ constraints}
Constraints of the form:
\[ \sum_{1 \leq i \leq n} x_i \bowtie 1 \]
\begin{description}
\item[\texttt{ExactlyOne}] \marginnote{\texttt{ExactlyOne}}
\[
\begin{split}
\texttt{ExactlyOne}([x_1, \dots, x_n]) &\iff \\
&\texttt{AtMostOne}([x_1, \dots, x_n]) \land \texttt{AtLeastOne}([x_1, \dots, x_n])
\end{split}
\]
\item[\texttt{AtLeastOne}] \marginnote{\texttt{AtLeastOne}}
\[ \texttt{AtLeastOne}([x_1, \dots, x_n]) \iff x_1 \vee x_2 \vee \dots \vee x_n \]
\item[\texttt{AtMostOne}] \marginnote{\texttt{AtMostOne}}
There are different encoding approaches:
\begin{description}
\item[Pairwise encoding] \marginnote{\texttt{AtMostOne} pairwise encoding}
Constrains the fact that any pair of variables cannot be both true:
\[ \texttt{AtMostOne}([x_1, \dots, x_n]) \iff \bigwedge_{1 \leq i < j \leq n} \lnot (x_i \land x_j) \]
This encoding does not require auxiliary variables and introduces $O(n^2)$ new clauses.
\item[Sequential encoding] \marginnote{\texttt{AtMostOne} sequential encoding}
Introduces $n$ new variables $s_i$ such that:
\begin{itemize}
\item If $s_i = 1$ and $s_{i-1} = 0$, then $x_i = 1$.
\item If $s_i = 1$ and $s_{i-1} = 1$, then $x_i = 0$.
\end{itemize}
\[
\begin{split}
\texttt{AtMostOne}([x_1, \dots, x_n]) &\iff \\
& (x_1 \Rightarrow s_1) \\
& \land \bigwedge_{1 < i < n} \left[ \big( (x_i \vee s_{i-1}) \Rightarrow s_i \big) \land (s_{i-1} \Rightarrow \lnot x_i) \right] \\
& \land (s_{n-1} \Rightarrow \lnot x_n)
\end{split}
\]
By expanding the implications, it becomes:
\[
\begin{split}
\texttt{AtMostOne}([x_1, \dots, x_n]) &\iff \\
& (\lnot x_1 \vee s_1) \\
& \land \bigwedge_{1 < i < n} \left[ (\lnot x_i \vee s_i) \land (\lnot s_{i-1} \vee s_i) \land (\lnot s_{i-1} \vee \lnot x_i) \right] \\
& \land (\lnot s_{n-1} \vee \lnot x_n)
\end{split}
\]
This encoding requires $O(n)$ auxiliary variables and $O(n)$ new clauses.
\item[Bitwise encoding] \marginnote{\texttt{AtMostOne} bitwise encoding}
Introduces $m = \log_2n$ new variables $r_i$ such that
if the variable $x_i$ is set to true, then $r_1, \dots, r_m$ contain the binary encoding of the index $i-1$.
Let $b_{i,1}, \dots, b_{i,m}$ be the $m$ bits of the binary representation of $i$, the encoding is the following:
\[
\begin{split}
\texttt{AtMostOne}([x_1, \dots, x_n]) &\iff \\
& \bigwedge_{1 \leq i \leq n} \big( x_i \Rightarrow (r_1 = b_{i-1,1} \land \dots \land r_m = b_{i-1,m}) \big)
\end{split}
\]
By expanding the implications, it becomes:
\[
\begin{split}
\texttt{AtMostOne}([x_1, \dots, x_n]) &\iff \\
& \bigwedge_{1 \leq i \leq n} \bigwedge_{1 \leq j \leq m} \big( \lnot x_i \vee (r_j = b_{i-1, j}) \big)
\end{split}
\]
This encoding requires $O(\log_2n)$ auxiliary variables and $O(n \log_2 n)$ new clauses.
\item[Heule encoding] \marginnote{\texttt{AtMostOne} Heule encoding}
Defines the encoding recursively:
\begin{itemize}
\item When $n \leq 4$, apply the pairwise encoding (which requires 6 clauses):
\[ \texttt{AtMostOne}([x_1, \dots, x_4]) \iff \bigwedge_{1 \leq i < j \leq n} \lnot (x_i \land x_j) \]
\item When $n > 4$, introduce a new variable $y$:
\[
\begin{split}
\texttt{AtMostOne}&([x_1, \dots, x_n]) \iff \\
&\texttt{AtMostOne}([x_1, x_2, x_3, y]) \land \texttt{AtMostOne}([\lnot y, x_4, \dots, x_n])
\end{split}
\]
\end{itemize}
This encoding requires $O(n)$ auxiliary variables and $O(n)$ new clauses.
\end{description}
\end{description}
\item[$\mathbf{k \in \mathbb{N}}$ constraints] \marginnote{$k \in \mathbb{N}$ constraints}
Constraints of the form:
\[ \sum_{1 \leq i \leq n} x_i \bowtie k \text{ where } k \in \mathbb{N} \]
\begin{theorem}
All the cardinality constraints can be expressed using \texttt{AtMostK} (i.e. $\leq$ relationship).
\begin{proof}
\[
\begin{split}
\sum_{1 \leq i \leq n} x_i = k &\iff \sum_{1 \leq i \leq n} (x_i \geq k ) \land \sum_{1 \leq i \leq n} (x_i \leq k) \\
\sum_{1 \leq i \leq n} x_i \neq k &\iff \sum_{1 \leq i \leq n} (x_i < k) \vee \sum_{1 \leq i \leq n} (x_i > k) \\
\sum_{1 \leq i \leq n} x_i \geq k &\iff \sum_{1 \leq i \leq n} (\lnot x_i \leq n-k) \\
\sum_{1 \leq i \leq n} x_i > k &\iff \sum_{1 \leq i \leq n} (\lnot x_i \leq n-k-1) \\
\sum_{1 \leq i \leq n} x_i < k &\iff \sum_{1 \leq i \leq n} (x_i \leq k-1)
\end{split}
\]
\end{proof}
\end{theorem}
\begin{description}
\item[\texttt{AtMostK}] \marginnote{\texttt{AtMostK}}
There are different encoding approaches:
\begin{description}
\item[Generalized pairwise encoding] \marginnote{\texttt{AtMostK} generalized pairwise encoding}
Constrains the fact that any pair of $(k+1)$ variables cannot be all true:
\[
\texttt{AtMostK}([x_1, \dots, x_n], k) \iff \bigwedge_{\substack{ M \subseteq \{ 1, \dots, n \}\\\vert M \vert = k+1 }} \bigvee_{i \in M} \lnot x_i
\]
This encoding does not require auxiliary variables and introduces $O(n^{k+1})$ new clauses.
\item[Sequential encoding] \marginnote{\texttt{AtMostK} sequential encoding}
Introduces $n \cdot k$ new variables $s_{i,j}$ such that:
\begin{itemize}
\item If $s_{i,j} = 1$ and $s_{i-1,j} = 0$, then $x_i$ is the $j$-th variable assigned to true.
\item If $s_{i,j} = 1$ and $s_{i-1,j} = 1$, then $x_i = 0$ and there are $j$ variables assigned to true among $x_1, \dots, x_{i-1}$.
\end{itemize}
\[
\begin{split}
\texttt{AtMostK}&([x_1, \dots, x_n], k) \iff \\
& (x_1 \Rightarrow s_{1,1}) \land \bigwedge_{2 \leq j \leq k} \lnot s_{1,j} \\
& \land \bigwedge_{1 < i < n} \left[
\begin{split}
& \big( (x_i \vee s_{i-1,1}) \Rightarrow s_{i,1} \big) \\
& \land \bigwedge_{2 \leq j \leq k} \Big( \big( (x_i \land s_{i-1, j-1}) \vee s_{i-1,j} \big) \Rightarrow s_{i,j} \Big) \\
& \land (s_{i-1,k} \Rightarrow \lnot x_i)
\end{split}
\right] \\
& \land (s_{n-1, k} \Rightarrow \lnot x_n)
\end{split}
\]
This encoding requires $O(nk)$ auxiliary variables and $O(nk)$ new clauses.
\end{description}
\end{description}
\item[Arc-consistency] \marginnote{Arc-consistency}
Given a SAT encoding $E$ of a normal constraint $C$,
$E$ is arc-consistent if:
\begin{itemize}
\item Whenever a partial assignment is inconsistent in $C$, unit resolution in $E$ causes a contradiction.
\item Otherwise, unit resolution in $E$ discards arc-inconsistent values.
\end{itemize}
\end{description}