Skip to content

Instantly share code, notes, and snippets.

@N-Coder

N-Coder/Volkswagen.ipynb

Last active December 8, 2022 13:34
Show Gist options
  • Save N-Coder/2e2904cc4ff3b1053c076c31bd729a73 to your computer and use it in GitHub Desktop.
Save N-Coder/2e2904cc4ff3b1053c076c31bd729a73 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
postBuild
#!/bin/bash
set -e
pysmt-install --check
pysmt-install --msat --confirm-agreement
pysmt-install --check
Raw
requirements.txt
ogdf-python
ogdf-wheel
pysmt
Display the source blob
Display the rendered blob
Raw
Volkswagen.ipynb
{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"id": "f94438cd",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Volkswagen problem proposed by Honsa\n",
"[Felix K., Diana S., Niko F., Peter S., Matthias P. 2022]\n"
]
}
],
"source": [
"print(\"Volkswagen problem proposed by Honsa\")\n",
"\n",
"authors = [\n",
" \"Matthias P.\",\n",
" \"Peter S.\",\n",
" \"Felix K.\",\n",
" \"Diana S.\",\n",
" \"Niko F.\"\n",
"]\n",
"\n",
"import random\n",
"random.shuffle(authors)\n",
"import datetime\n",
"\n",
"print(\"[%s %s]\" % (\", \".join(authors), datetime.datetime.now().year))"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "f7202c44",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [],
"source": [
"import itertools\n",
"import random\n",
"from collections import defaultdict\n",
"\n",
"from ogdf_python import ogdf\n",
"import pysmt.shortcuts as sat\n",
"\n",
"NoArrow = getattr(ogdf.EdgeArrow, \"None\")\n",
"\n",
"def powerset(iterable):\n",
" s = list(iterable)\n",
" return itertools.chain.from_iterable(itertools.combinations(s, r) for r in range(len(s)+1))"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "bc1b4099",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [],
"source": [
"class Volkswagen:\n",
" def make_graph(self, u, l):\n",
" self.G = ogdf.Graph()\n",
" self.GA = ogdf.GraphAttributes(self.G, ogdf.GraphAttributes.all)\n",
" self.upper = [self.G.newNode() for _ in range(u)]\n",
" self.lower = [self.G.newNode() for _ in range(l)]\n",
" self.GA.directed = False # TODO widget\n",
"\n",
" def layout(self, d=50):\n",
" GA = self.GA\n",
" self.w = max(len(self.upper) + 1, len(self.lower) + 1) * d\n",
" self.h = -200\n",
"\n",
" self.border_lines = lines = [self.G.newNode() for _ in range(4)]\n",
" self.border_edges = edges = (self.G.newEdge(lines[0], lines[1]), self.G.newEdge(lines[2], lines[3]))\n",
" GA.strokeType[edges[0]] = GA.strokeType[edges[1]] = ogdf.StrokeType.Dot # TODO widget\n",
" GA.strokeWidth[edges[0]] = GA.strokeWidth[edges[1]] = 5\n",
" GA.strokeColor[edges[0]] = GA.strokeColor[edges[1]] = ogdf.Color(\"#CCC\")\n",
" GA.arrowType[edges[0]] = GA.arrowType[edges[1]] = NoArrow\n",
" \n",
" GA.x[lines[0]], GA.y[lines[0]] = 0, self.h\n",
" GA.x[lines[1]], GA.y[lines[1]] = self.w, self.h\n",
" GA.label[lines[0]] = \"U\"\n",
" GA.x[lines[2]], GA.y[lines[2]] = 0, 0\n",
" GA.x[lines[3]], GA.y[lines[3]] = self.w, 0\n",
" GA.label[lines[2]] = \"L\"\n",
" GA.width[lines[1]] = GA.height[lines[1]] = 0\n",
" GA.width[lines[3]] = GA.height[lines[3]] = 0\n",
" \n",
" for i, v in enumerate(self.upper):\n",
" GA.label[v] = str(i)\n",
" GA.yLabel[v] = -10\n",
" GA.shape[v] = ogdf.Shape.Ellipse\n",
" GA.width[v] = GA.height[v] = 10\n",
" GA.x[v], GA.y[v] = (i + 1) * d, self.h\n",
" for i, v in enumerate(self.lower):\n",
" GA.label[v] = str(i)\n",
" GA.yLabel[v] = 12\n",
" GA.shape[v] = ogdf.Shape.Ellipse\n",
" GA.width[v] = GA.height[v] = 10\n",
" GA.x[v], GA.y[v] = (i + 1) * d, 0\n",
"\n",
" def sort(self, perm):\n",
" for i, v in enumerate(perm):\n",
" self.GA.x[v] = (i + 1) * 50\n",
" \n",
" def get_label(self, n):\n",
" if not n:\n",
" return n\n",
" elif isinstance(n, tuple):\n",
" return tuple(self.get_label(x) for x in n)\n",
" else:\n",
" return (\"U\" if self.GA.y[n] < 0 else \"L\") + self.GA.label[n].decode(\"ascii\")\n",
"\n",
" ###\n",
"\n",
" def new_edge(self, u, v, c=None):\n",
" if isinstance(u, int):\n",
" u = self.upper[u]\n",
" if isinstance(v, int):\n",
" v = self.lower[v]\n",
" e = self.G.newEdge(u, v)\n",
" self.GA.strokeWidth[e] = 3\n",
" if c:\n",
" self.GA.strokeColor[e] = c\n",
" self.GA.arrowType[e] = NoArrow\n",
" return e\n",
"\n",
" def gadget(self, t, b, c):\n",
" t1, t2, t3 = [self.upper[x] if isinstance(x, int) else x for x in t]\n",
" b1, b2, b3 = [self.lower[x] if isinstance(x, int) else x for x in b]\n",
" edges = [\n",
" self.new_edge(u, v, c) for u, v in\n",
" [(t1, b2), (b2, t3), (b1, t2), (t2, b3), (t2, b2)]\n",
" ]\n",
" self.GA.strokeType[edges[-1]] = ogdf.StrokeType.Dash\n",
" self.GA.strokeWidth[edges[-1]] = 1\n",
"\n",
" def swap(self, a, b):\n",
" if isinstance(a, int):\n",
" a = self.lower[a]\n",
" if isinstance(b, int):\n",
" b = self.lower[b]\n",
" GA = self.GA\n",
" (GA.x[a], GA.y[a]), (GA.x[b], GA.y[b]) = (GA.x[b], GA.y[b]), (GA.x[a], GA.y[a])\n",
"\n",
" ###\n",
"\n",
" def is_dashed(self, e):\n",
" return ord(self.GA.strokeType[e]) in [ogdf.StrokeType.Dash, ogdf.StrokeType.Dot]\n",
" \n",
" def get_edges(self):\n",
" return [(self.get_label(e.source()), self.get_label(e.target())) for e in self.G.edges if not self.is_dashed(e)]\n",
" \n",
" def has_edge(self, u, v):\n",
" if isinstance(u, int):\n",
" u = self.upper[u]\n",
" if isinstance(v, int):\n",
" v = self.lower[v]\n",
" e = self.G.searchEdge(u, v)\n",
" if not e:\n",
" return False\n",
" elif self.is_dashed(e):\n",
" return False\n",
" else:\n",
" return True\n",
"\n",
" def check(self, **kwargs):\n",
" l = list(self.find_vw(**kwargs, multi=False))\n",
" if l:\n",
" return l[0]\n",
" else:\n",
" return None\n",
" \n",
" def find_vw(self, do_print=False, mark=False, multi=False):\n",
" GA = self.GA\n",
" for u in self.upper:\n",
" for l in self.lower:\n",
" if u.degree() == 0 or l.degree() == 0 or self.has_edge(u, l):\n",
" continue\n",
" upper_left = [GA.label[a.twinNode()] for a in l.adjEntries if GA.x[a.twinNode()] < GA.x[u]]\n",
" upper_right = [GA.label[a.twinNode()] for a in l.adjEntries if GA.x[a.twinNode()] > GA.x[u]]\n",
" lower_left = [GA.label[a.twinNode()] for a in u.adjEntries if GA.x[a.twinNode()] < GA.x[l]]\n",
" lower_right = [GA.label[a.twinNode()] for a in u.adjEntries if GA.x[a.twinNode()] > GA.x[l]]\n",
" sets = (upper_left, upper_right, lower_left, lower_right)\n",
" if do_print:\n",
" print(\"Non-Edge\", GA.label[u], GA.label[l])\n",
" print(\"upper_left\", upper_left)\n",
" print(\"upper_right\", upper_right)\n",
" print(\"lower_left\", lower_left)\n",
" print(\"lower_right\", lower_right)\n",
" if all(sets):\n",
" # TODO mark\n",
" yield u, l, sets\n",
" if not multi:\n",
" break\n",
"\n",
" def try_all(self, only_one=False):\n",
" xs = [self.GA.x[v] for v in self.lower]\n",
" low_deg = [v for v in self.lower if v.degree() == 0]\n",
" for perm in itertools.permutations(v for v in self.lower if v.degree() > 0):\n",
" perm = [*perm, *low_deg]\n",
" self.sort(perm)\n",
" if not self.check():\n",
" # print([self.GA.label(v).encode() for v in perm])\n",
" yield perm\n",
" if only_one:\n",
" break\n",
" for v, x in zip(self.lower, xs):\n",
" self.GA.x[v] = x\n",
"\n",
" def sat_constraints(self, do_print=False):\n",
" for l in self.lower:\n",
" if l.degree() < 2:\n",
" continue\n",
" first = min(l.adjEntries, key=lambda a: self.GA.x[a.twinNode()])\n",
" last = max(l.adjEntries, key=lambda a: self.GA.x[a.twinNode()])\n",
" if do_print:\n",
" print(self.get_label(l),\":\",self.get_label(first.twinNode()),\"->\",self.get_label(last.twinNode()))\n",
" for u in self.upper:\n",
" if u.degree() < 2:\n",
" continue\n",
" if self.GA.x[u] < self.GA.x[first.twinNode()] or self.GA.x[u] > self.GA.x[last.twinNode()]:\n",
" continue\n",
" if self.has_edge(l, u):\n",
" continue\n",
" if do_print:\n",
" print(\" \", self.get_label(l), \"-\", self.get_label(u), [self.get_label(a.twinNode()) for a in u.adjEntries if a.twinNode() != l])\n",
" yield l, u\n",
"\n",
"\n",
" def sat_dict(self):\n",
" d = defaultdict(list)\n",
" for l, u in self.sat_constraints():\n",
" d[self.GA.label[l]].extend([self.GA.label[a.twinNode()] for a in u.adjEntries if a.twinNode() != l])\n",
" return d\n",
"\n",
" def sat_cnf(self, trans=False):\n",
" pos = {}\n",
" clauses = []\n",
" \n",
" def mkpair(l, l2):\n",
" if (l, l2) not in pos:\n",
" a = pos[(l, l2)] = sat.Symbol(self.get_label(l) + \" < \" + self.get_label(l2))\n",
" b = pos[(l2, l)] = sat.Symbol(self.get_label(l2) + \" < \" + self.get_label(l))\n",
" clauses.append(sat.Iff(a, sat.Not(b)))\n",
" return a\n",
" else:\n",
" return pos[(l, l2)]\n",
" \n",
" for l, u in self.sat_constraints():\n",
" sync = sat.Symbol(\"%s < [%s]\" % (self.get_label(l),\n",
" \", \".join(self.get_label(a.twinNode()) for a in u.adjEntries if a.twinNode() != l)))\n",
" for a in u.adjEntries:\n",
" if a.twinNode() == l:\n",
" continue\n",
" clauses.append(sat.Iff(sync, mkpair(l, a.twinNode())))\n",
" if not trans:\n",
" return sat.And(clauses)\n",
" \n",
" pairs = [(a,b) for a,b in pos.keys() if a.index() < b.index()]\n",
" for (a,b),(c,d) in itertools.combinations(pairs, 2):\n",
" elems = {a,b,c,d}\n",
" if len(elems) != 3:\n",
" continue\n",
" a,b,c = elems\n",
" clauses.append(sat.Implies(\n",
" sat.And(mkpair(a,b), mkpair(b,c)),\n",
" mkpair(a,c)\n",
" ))\n",
" clauses.append(sat.Implies(\n",
" sat.And(mkpair(b,a), mkpair(c,b)),\n",
" mkpair(c,a)\n",
" ))\n",
" return sat.And(clauses)\n",
"\n",
" def sat_solvable(self, **kwds):\n",
" return sat.is_sat(self.sat_cnf(**kwds))"
]
},
{
"cell_type": "code",
"execution_count": 138,
"id": "8b2a8f91",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"data": {
"text/plain": "<cppyy.gbl.ogdf.GraphAttributes object at 0x556e04c4b430>",
"text/html": "<?xml version=\"1.0\"?>\n<svg xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" xmlns:ev=\"http://www.w3.org/2001/xml-events\" version=\"1.1\" baseProfile=\"full\" viewBox=\"-60.5 -260.5 411 321\">\n\t<g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M0,-200 L300,-200\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M0,0 L300,0\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M100,-200 L150,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M150,0 L200,-200\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M100,0 L150,-200\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M150,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M150,-200 L150,0\" stroke=\"#00FF00\" stroke-width=\"1.000000px\" stroke-dasharray=\"4,2\" />\n\t\t</g>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"50\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"50\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"100\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"100\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"150\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"150\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"200\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"200\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"250\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"250\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"50\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"50\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"100\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"100\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"150\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"150\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"200\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"200\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"250\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"250\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n\t</g>\n\t<g>\n\t\t<rect x=\"-10\" y=\"-210\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"0\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">U</text>\n\t</g>\n\t<g>\n\t\t<rect x=\"300\" y=\"-200\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"300\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n\t</g>\n\t<g>\n\t\t<rect x=\"-10\" y=\"-10\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"0\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">L</text>\n\t</g>\n\t<g>\n\t\t<rect x=\"300\" y=\"0\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"300\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n\t</g>\n</svg>\n"
},
"execution_count": 138,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"VW = Volkswagen()\n",
"VW.make_graph(5, 5)\n",
"VW.layout()\n",
"VW.gadget((1,2,3),(1,2,3),ogdf.Color(\"#0F0\"))\n",
"VW.GA"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "77c088c6",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"data": {
"text/html": [
"<?xml version=\"1.0\"?>\n",
"<svg xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" xmlns:ev=\"http://www.w3.org/2001/xml-events\" version=\"1.1\" baseProfile=\"full\" viewBox=\"-60.5 -260.5 411 321\">\n",
"\t<g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M0,-200 L300,-200\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M0,0 L300,0\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M100,-200 L100,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M100,0 L200,-200\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M150,0 L150,-200\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M150,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M150,-200 L100,0\" stroke=\"#00FF00\" stroke-width=\"1.000000px\" stroke-dasharray=\"4,2\" />\n",
"\t\t</g>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"50\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"50\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"100\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"100\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"150\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"150\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"200\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"200\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"250\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"250\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"50\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"50\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"150\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"150\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"100\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"100\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"200\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"200\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"250\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"250\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"-10\" y=\"-210\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"0\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">U</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"300\" y=\"-200\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"300\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"-10\" y=\"-10\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"0\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">L</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"300\" y=\"0\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"300\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n",
"\t</g>\n",
"</svg>\n"
],
"text/plain": [
"<cppyy.gbl.ogdf.GraphAttributes object at 0x556dfbad7980>"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"VW.swap(1,2)\n",
"VW.GA"
]
},
{
"cell_type": "code",
"execution_count": 71,
"id": "82837b25",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"data": {
"text/plain": [
"[\"('L0 < L19' <-> (! 'L19 < L0'))\",\n",
" \"('L0 < L2' <-> (! 'L2 < L0'))\",\n",
" \"('L0 < L3' <-> (! 'L3 < L0'))\",\n",
" \"('L0 < L6' <-> (! 'L6 < L0'))\",\n",
" \"('L0 < L7' <-> (! 'L7 < L0'))\",\n",
" \"('L0 < L8' <-> (! 'L8 < L0'))\",\n",
" \"('L0 < L9' <-> (! 'L9 < L0'))\",\n",
" \"('L0 < [L2, L8, L9]' <-> 'L0 < L2')\",\n",
" \"('L0 < [L2, L8, L9]' <-> 'L0 < L8')\",\n",
" \"('L0 < [L2, L8, L9]' <-> 'L0 < L9')\",\n",
" \"('L0 < [L3, L6, L7, L9, L19]' <-> 'L0 < L19')\",\n",
" \"('L0 < [L3, L6, L7, L9, L19]' <-> 'L0 < L3')\",\n",
" \"('L0 < [L3, L6, L7, L9, L19]' <-> 'L0 < L6')\",\n",
" \"('L0 < [L3, L6, L7, L9, L19]' <-> 'L0 < L7')\",\n",
" \"('L0 < [L3, L6, L7, L9, L19]' <-> 'L0 < L9')\",\n",
" \"('L1 < L0' <-> (! 'L0 < L1'))\",\n",
" \"('L1 < L10' <-> (! 'L10 < L1'))\",\n",
" \"('L1 < L11' <-> (! 'L11 < L1'))\",\n",
" \"('L1 < L13' <-> (! 'L13 < L1'))\",\n",
" \"('L1 < L14' <-> (! 'L14 < L1'))\",\n",
" \"('L1 < L15' <-> (! 'L15 < L1'))\",\n",
" \"('L1 < L16' <-> (! 'L16 < L1'))\",\n",
" \"('L1 < L17' <-> (! 'L17 < L1'))\",\n",
" \"('L1 < L18' <-> (! 'L18 < L1'))\",\n",
" \"('L1 < L2' <-> (! 'L2 < L1'))\",\n",
" \"('L1 < L3' <-> (! 'L3 < L1'))\",\n",
" \"('L1 < L4' <-> (! 'L4 < L1'))\",\n",
" \"('L1 < L5' <-> (! 'L5 < L1'))\",\n",
" \"('L1 < L6' <-> (! 'L6 < L1'))\",\n",
" \"('L1 < [L10, L13, L15]' <-> 'L1 < L10')\",\n",
" \"('L1 < [L10, L13, L15]' <-> 'L1 < L13')\",\n",
" \"('L1 < [L10, L13, L15]' <-> 'L1 < L15')\",\n",
" \"('L1 < [L3, L4, L10, L11, L18]' <-> 'L1 < L10')\",\n",
" \"('L1 < [L3, L4, L10, L11, L18]' <-> 'L1 < L11')\",\n",
" \"('L1 < [L3, L4, L10, L11, L18]' <-> 'L1 < L18')\",\n",
" \"('L1 < [L3, L4, L10, L11, L18]' <-> 'L1 < L3')\",\n",
" \"('L1 < [L3, L4, L10, L11, L18]' <-> 'L1 < L4')\",\n",
" \"('L1 < [L4, L6, L10, L16]' <-> 'L1 < L10')\",\n",
" \"('L1 < [L4, L6, L10, L16]' <-> 'L1 < L16')\",\n",
" \"('L1 < [L4, L6, L10, L16]' <-> 'L1 < L4')\",\n",
" \"('L1 < [L4, L6, L10, L16]' <-> 'L1 < L6')\",\n",
" \"('L1 < [L5, L10, L13]' <-> 'L1 < L10')\",\n",
" \"('L1 < [L5, L10, L13]' <-> 'L1 < L13')\",\n",
" \"('L1 < [L5, L10, L13]' <-> 'L1 < L5')\",\n",
" \"('L10 < L0' <-> (! 'L0 < L10'))\",\n",
" \"('L10 < L11' <-> (! 'L11 < L10'))\",\n",
" \"('L10 < L12' <-> (! 'L12 < L10'))\",\n",
" \"('L10 < L13' <-> (! 'L13 < L10'))\",\n",
" \"('L10 < L14' <-> (! 'L14 < L10'))\",\n",
" \"('L10 < L18' <-> (! 'L18 < L10'))\",\n",
" \"('L10 < [L1, L7, L14]' <-> 'L10 < L1')\",\n",
" \"('L10 < [L1, L7, L14]' <-> 'L10 < L14')\",\n",
" \"('L10 < [L1, L7, L14]' <-> 'L10 < L7')\",\n",
" \"('L10 < [L4, L7, L8, L13, L14, L18]' <-> 'L10 < L13')\",\n",
" \"('L10 < [L4, L7, L8, L13, L14, L18]' <-> 'L10 < L14')\",\n",
" \"('L10 < [L4, L7, L8, L13, L14, L18]' <-> 'L10 < L18')\",\n",
" \"('L10 < [L4, L7, L8, L13, L14, L18]' <-> 'L10 < L4')\",\n",
" \"('L10 < [L4, L7, L8, L13, L14, L18]' <-> 'L10 < L7')\",\n",
" \"('L10 < [L4, L7, L8, L13, L14, L18]' <-> 'L10 < L8')\",\n",
" \"('L10 < [L8, L9, L12, L13]' <-> 'L10 < L12')\",\n",
" \"('L10 < [L8, L9, L12, L13]' <-> 'L10 < L13')\",\n",
" \"('L10 < [L8, L9, L12, L13]' <-> 'L10 < L8')\",\n",
" \"('L10 < [L8, L9, L12, L13]' <-> 'L10 < L9')\",\n",
" \"('L11 < L0' <-> (! 'L0 < L11'))\",\n",
" \"('L11 < L15' <-> (! 'L15 < L11'))\",\n",
" \"('L11 < L18' <-> (! 'L18 < L11'))\",\n",
" \"('L11 < L6' <-> (! 'L6 < L11'))\",\n",
" \"('L12 < L0' <-> (! 'L0 < L12'))\",\n",
" \"('L12 < L1' <-> (! 'L1 < L12'))\",\n",
" \"('L12 < L11' <-> (! 'L11 < L12'))\",\n",
" \"('L12 < L13' <-> (! 'L13 < L12'))\",\n",
" \"('L12 < L14' <-> (! 'L14 < L12'))\",\n",
" \"('L12 < L15' <-> (! 'L15 < L12'))\",\n",
" \"('L12 < L16' <-> (! 'L16 < L12'))\",\n",
" \"('L12 < L17' <-> (! 'L17 < L12'))\",\n",
" \"('L12 < L18' <-> (! 'L18 < L12'))\",\n",
" \"('L12 < [L1, L5, L6, L10, L14, L17]' <-> 'L12 < L1')\",\n",
" \"('L12 < [L1, L5, L6, L10, L14, L17]' <-> 'L12 < L10')\",\n",
" \"('L12 < [L1, L5, L6, L10, L14, L17]' <-> 'L12 < L14')\",\n",
" \"('L12 < [L1, L5, L6, L10, L14, L17]' <-> 'L12 < L17')\",\n",
" \"('L12 < [L1, L5, L6, L10, L14, L17]' <-> 'L12 < L5')\",\n",
" \"('L12 < [L1, L5, L6, L10, L14, L17]' <-> 'L12 < L6')\",\n",
" \"('L12 < [L1, L7, L14]' <-> 'L12 < L1')\",\n",
" \"('L12 < [L1, L7, L14]' <-> 'L12 < L14')\",\n",
" \"('L12 < [L1, L7, L14]' <-> 'L12 < L7')\",\n",
" \"('L12 < [L10, L13, L15]' <-> 'L12 < L10')\",\n",
" \"('L12 < [L10, L13, L15]' <-> 'L12 < L13')\",\n",
" \"('L12 < [L10, L13, L15]' <-> 'L12 < L15')\",\n",
" \"('L12 < [L3, L4, L10, L11, L18]' <-> 'L12 < L10')\",\n",
" \"('L12 < [L3, L4, L10, L11, L18]' <-> 'L12 < L11')\",\n",
" \"('L12 < [L3, L4, L10, L11, L18]' <-> 'L12 < L18')\",\n",
" \"('L12 < [L3, L4, L10, L11, L18]' <-> 'L12 < L3')\",\n",
" \"('L12 < [L3, L4, L10, L11, L18]' <-> 'L12 < L4')\",\n",
" \"('L12 < [L4, L6, L10, L16]' <-> 'L12 < L10')\",\n",
" \"('L12 < [L4, L6, L10, L16]' <-> 'L12 < L16')\",\n",
" \"('L12 < [L4, L6, L10, L16]' <-> 'L12 < L4')\",\n",
" \"('L12 < [L4, L6, L10, L16]' <-> 'L12 < L6')\",\n",
" \"('L12 < [L5, L10, L13]' <-> 'L12 < L10')\",\n",
" \"('L12 < [L5, L10, L13]' <-> 'L12 < L13')\",\n",
" \"('L12 < [L5, L10, L13]' <-> 'L12 < L5')\",\n",
" \"('L13 < L0' <-> (! 'L0 < L13'))\",\n",
" \"('L13 < L11' <-> (! 'L11 < L13'))\",\n",
" \"('L13 < L14' <-> (! 'L14 < L13'))\",\n",
" \"('L13 < L15' <-> (! 'L15 < L13'))\",\n",
" \"('L13 < L16' <-> (! 'L16 < L13'))\",\n",
" \"('L13 < L17' <-> (! 'L17 < L13'))\",\n",
" \"('L13 < L18' <-> (! 'L18 < L13'))\",\n",
" \"('L13 < [L1, L5, L6, L10, L14, L17]' <-> 'L13 < L1')\",\n",
" \"('L13 < [L1, L5, L6, L10, L14, L17]' <-> 'L13 < L10')\",\n",
" \"('L13 < [L1, L5, L6, L10, L14, L17]' <-> 'L13 < L14')\",\n",
" \"('L13 < [L1, L5, L6, L10, L14, L17]' <-> 'L13 < L17')\",\n",
" \"('L13 < [L1, L5, L6, L10, L14, L17]' <-> 'L13 < L5')\",\n",
" \"('L13 < [L1, L5, L6, L10, L14, L17]' <-> 'L13 < L6')\",\n",
" \"('L13 < [L1, L7, L14]' <-> 'L13 < L1')\",\n",
" \"('L13 < [L1, L7, L14]' <-> 'L13 < L14')\",\n",
" \"('L13 < [L1, L7, L14]' <-> 'L13 < L7')\",\n",
" \"('L13 < [L3, L4, L10, L11, L18]' <-> 'L13 < L10')\",\n",
" \"('L13 < [L3, L4, L10, L11, L18]' <-> 'L13 < L11')\",\n",
" \"('L13 < [L3, L4, L10, L11, L18]' <-> 'L13 < L18')\",\n",
" \"('L13 < [L3, L4, L10, L11, L18]' <-> 'L13 < L3')\",\n",
" \"('L13 < [L3, L4, L10, L11, L18]' <-> 'L13 < L4')\",\n",
" \"('L13 < [L3, L5, L8]' <-> 'L13 < L3')\",\n",
" \"('L13 < [L3, L5, L8]' <-> 'L13 < L5')\",\n",
" \"('L13 < [L3, L5, L8]' <-> 'L13 < L8')\",\n",
" \"('L13 < [L4, L12, L14]' <-> 'L13 < L12')\",\n",
" \"('L13 < [L4, L12, L14]' <-> 'L13 < L14')\",\n",
" \"('L13 < [L4, L12, L14]' <-> 'L13 < L4')\",\n",
" \"('L13 < [L4, L6, L10, L16]' <-> 'L13 < L10')\",\n",
" \"('L13 < [L4, L6, L10, L16]' <-> 'L13 < L16')\",\n",
" \"('L13 < [L4, L6, L10, L16]' <-> 'L13 < L4')\",\n",
" \"('L13 < [L4, L6, L10, L16]' <-> 'L13 < L6')\",\n",
" \"('L14 < L0' <-> (! 'L0 < L14'))\",\n",
" \"('L14 < L11' <-> (! 'L11 < L14'))\",\n",
" \"('L14 < L15' <-> (! 'L15 < L14'))\",\n",
" \"('L14 < L16' <-> (! 'L16 < L14'))\",\n",
" \"('L14 < L18' <-> (! 'L18 < L14'))\",\n",
" \"('L14 < [L10, L13, L15]' <-> 'L14 < L10')\",\n",
" \"('L14 < [L10, L13, L15]' <-> 'L14 < L13')\",\n",
" \"('L14 < [L10, L13, L15]' <-> 'L14 < L15')\",\n",
" \"('L14 < [L3, L4, L10, L11, L18]' <-> 'L14 < L10')\",\n",
" \"('L14 < [L3, L4, L10, L11, L18]' <-> 'L14 < L11')\",\n",
" \"('L14 < [L3, L4, L10, L11, L18]' <-> 'L14 < L18')\",\n",
" \"('L14 < [L3, L4, L10, L11, L18]' <-> 'L14 < L3')\",\n",
" \"('L14 < [L3, L4, L10, L11, L18]' <-> 'L14 < L4')\",\n",
" \"('L14 < [L4, L6, L10, L16]' <-> 'L14 < L10')\",\n",
" \"('L14 < [L4, L6, L10, L16]' <-> 'L14 < L16')\",\n",
" \"('L14 < [L4, L6, L10, L16]' <-> 'L14 < L4')\",\n",
" \"('L14 < [L4, L6, L10, L16]' <-> 'L14 < L6')\",\n",
" \"('L14 < [L5, L10, L13]' <-> 'L14 < L10')\",\n",
" \"('L14 < [L5, L10, L13]' <-> 'L14 < L13')\",\n",
" \"('L14 < [L5, L10, L13]' <-> 'L14 < L5')\",\n",
" \"('L14 < [L8, L9, L12, L13]' <-> 'L14 < L12')\",\n",
" \"('L14 < [L8, L9, L12, L13]' <-> 'L14 < L13')\",\n",
" \"('L14 < [L8, L9, L12, L13]' <-> 'L14 < L8')\",\n",
" \"('L14 < [L8, L9, L12, L13]' <-> 'L14 < L9')\",\n",
" \"('L15 < L0' <-> (! 'L0 < L15'))\",\n",
" \"('L15 < L10' <-> (! 'L10 < L15'))\",\n",
" \"('L15 < L17' <-> (! 'L17 < L15'))\",\n",
" \"('L15 < L18' <-> (! 'L18 < L15'))\",\n",
" \"('L15 < [L1, L5, L6, L10, L14, L17]' <-> 'L15 < L1')\",\n",
" \"('L15 < [L1, L5, L6, L10, L14, L17]' <-> 'L15 < L10')\",\n",
" \"('L15 < [L1, L5, L6, L10, L14, L17]' <-> 'L15 < L14')\",\n",
" \"('L15 < [L1, L5, L6, L10, L14, L17]' <-> 'L15 < L17')\",\n",
" \"('L15 < [L1, L5, L6, L10, L14, L17]' <-> 'L15 < L5')\",\n",
" \"('L15 < [L1, L5, L6, L10, L14, L17]' <-> 'L15 < L6')\",\n",
" \"('L16 < L0' <-> (! 'L0 < L16'))\",\n",
" \"('L16 < L10' <-> (! 'L10 < L16'))\",\n",
" \"('L16 < L11' <-> (! 'L11 < L16'))\",\n",
" \"('L16 < L15' <-> (! 'L15 < L16'))\",\n",
" \"('L16 < L17' <-> (! 'L17 < L16'))\",\n",
" \"('L16 < L18' <-> (! 'L18 < L16'))\",\n",
" \"('L16 < L2' <-> (! 'L2 < L16'))\",\n",
" \"('L16 < L4' <-> (! 'L4 < L16'))\",\n",
" \"('L16 < [L1, L5, L6, L10, L14, L17]' <-> 'L16 < L1')\",\n",
" \"('L16 < [L1, L5, L6, L10, L14, L17]' <-> 'L16 < L10')\",\n",
" \"('L16 < [L1, L5, L6, L10, L14, L17]' <-> 'L16 < L14')\",\n",
" \"('L16 < [L1, L5, L6, L10, L14, L17]' <-> 'L16 < L17')\",\n",
" \"('L16 < [L1, L5, L6, L10, L14, L17]' <-> 'L16 < L5')\",\n",
" \"('L16 < [L1, L5, L6, L10, L14, L17]' <-> 'L16 < L6')\",\n",
" \"('L16 < [L10, L13, L15]' <-> 'L16 < L10')\",\n",
" \"('L16 < [L10, L13, L15]' <-> 'L16 < L13')\",\n",
" \"('L16 < [L10, L13, L15]' <-> 'L16 < L15')\",\n",
" \"('L16 < [L3, L5, L8]' <-> 'L16 < L3')\",\n",
" \"('L16 < [L3, L5, L8]' <-> 'L16 < L5')\",\n",
" \"('L16 < [L3, L5, L8]' <-> 'L16 < L8')\",\n",
" \"('L16 < [L4, L12, L14]' <-> 'L16 < L12')\",\n",
" \"('L16 < [L4, L12, L14]' <-> 'L16 < L14')\",\n",
" \"('L16 < [L4, L12, L14]' <-> 'L16 < L4')\",\n",
" \"('L17 < L0' <-> (! 'L0 < L17'))\",\n",
" \"('L17 < L10' <-> (! 'L10 < L17'))\",\n",
" \"('L17 < L11' <-> (! 'L11 < L17'))\",\n",
" \"('L17 < L14' <-> (! 'L14 < L17'))\",\n",
" \"('L17 < L18' <-> (! 'L18 < L17'))\",\n",
" \"('L17 < L19' <-> (! 'L19 < L17'))\",\n",
" \"('L17 < L2' <-> (! 'L2 < L17'))\",\n",
" \"('L17 < L5' <-> (! 'L5 < L17'))\",\n",
" \"('L17 < L6' <-> (! 'L6 < L17'))\",\n",
" \"('L17 < [L0, L2, L13, L16]' <-> 'L17 < L0')\",\n",
" \"('L17 < [L0, L2, L13, L16]' <-> 'L17 < L13')\",\n",
" \"('L17 < [L0, L2, L13, L16]' <-> 'L17 < L16')\",\n",
" \"('L17 < [L0, L2, L13, L16]' <-> 'L17 < L2')\",\n",
" \"('L17 < [L0, L9]' <-> 'L17 < L0')\",\n",
" \"('L17 < [L0, L9]' <-> 'L17 < L9')\",\n",
" \"('L17 < [L10, L13, L15]' <-> 'L17 < L10')\",\n",
" \"('L17 < [L10, L13, L15]' <-> 'L17 < L13')\",\n",
" \"('L17 < [L10, L13, L15]' <-> 'L17 < L15')\",\n",
" \"('L17 < [L2, L8, L9]' <-> 'L17 < L2')\",\n",
" \"('L17 < [L2, L8, L9]' <-> 'L17 < L8')\",\n",
" \"('L17 < [L2, L8, L9]' <-> 'L17 < L9')\",\n",
" \"('L17 < [L3, L4, L10, L11, L18]' <-> 'L17 < L10')\",\n",
" \"('L17 < [L3, L4, L10, L11, L18]' <-> 'L17 < L11')\",\n",
" \"('L17 < [L3, L4, L10, L11, L18]' <-> 'L17 < L18')\",\n",
" \"('L17 < [L3, L4, L10, L11, L18]' <-> 'L17 < L3')\",\n",
" \"('L17 < [L3, L4, L10, L11, L18]' <-> 'L17 < L4')\",\n",
" \"('L17 < [L3, L5, L8]' <-> 'L17 < L3')\",\n",
" \"('L17 < [L3, L5, L8]' <-> 'L17 < L5')\",\n",
" \"('L17 < [L3, L5, L8]' <-> 'L17 < L8')\",\n",
" \"('L17 < [L3, L6, L7, L9, L19]' <-> 'L17 < L19')\",\n",
" \"('L17 < [L3, L6, L7, L9, L19]' <-> 'L17 < L3')\",\n",
" \"('L17 < [L3, L6, L7, L9, L19]' <-> 'L17 < L6')\",\n",
" \"('L17 < [L3, L6, L7, L9, L19]' <-> 'L17 < L7')\",\n",
" \"('L17 < [L3, L6, L7, L9, L19]' <-> 'L17 < L9')\",\n",
" \"('L17 < [L4, L12, L14]' <-> 'L17 < L12')\",\n",
" \"('L17 < [L4, L12, L14]' <-> 'L17 < L14')\",\n",
" \"('L17 < [L4, L12, L14]' <-> 'L17 < L4')\",\n",
" \"('L17 < [L4, L6, L10, L16]' <-> 'L17 < L10')\",\n",
" \"('L17 < [L4, L6, L10, L16]' <-> 'L17 < L16')\",\n",
" \"('L17 < [L4, L6, L10, L16]' <-> 'L17 < L4')\",\n",
" \"('L17 < [L4, L6, L10, L16]' <-> 'L17 < L6')\",\n",
" \"('L17 < [L5, L10, L13]' <-> 'L17 < L10')\",\n",
" \"('L17 < [L5, L10, L13]' <-> 'L17 < L13')\",\n",
" \"('L17 < [L5, L10, L13]' <-> 'L17 < L5')\",\n",
" \"('L17 < [L7, L9]' <-> 'L17 < L7')\",\n",
" \"('L17 < [L7, L9]' <-> 'L17 < L9')\",\n",
" \"('L18 < L0' <-> (! 'L0 < L18'))\",\n",
" \"('L18 < [L1, L7, L14]' <-> 'L18 < L1')\",\n",
" \"('L18 < [L1, L7, L14]' <-> 'L18 < L14')\",\n",
" \"('L18 < [L1, L7, L14]' <-> 'L18 < L7')\",\n",
" \"('L18 < [L8, L9, L12, L13]' <-> 'L18 < L12')\",\n",
" \"('L18 < [L8, L9, L12, L13]' <-> 'L18 < L13')\",\n",
" \"('L18 < [L8, L9, L12, L13]' <-> 'L18 < L8')\",\n",
" \"('L18 < [L8, L9, L12, L13]' <-> 'L18 < L9')\",\n",
" \"('L19 < L1' <-> (! 'L1 < L19'))\",\n",
" \"('L19 < L10' <-> (! 'L10 < L19'))\",\n",
" \"('L19 < L11' <-> (! 'L11 < L19'))\",\n",
" \"('L19 < L12' <-> (! 'L12 < L19'))\",\n",
" \"('L19 < L13' <-> (! 'L13 < L19'))\",\n",
" \"('L19 < L14' <-> (! 'L14 < L19'))\",\n",
" \"('L19 < L15' <-> (! 'L15 < L19'))\",\n",
" \"('L19 < L16' <-> (! 'L16 < L19'))\",\n",
" \"('L19 < L18' <-> (! 'L18 < L19'))\",\n",
" \"('L19 < L3' <-> (! 'L3 < L19'))\",\n",
" \"('L19 < L4' <-> (! 'L4 < L19'))\",\n",
" \"('L19 < L5' <-> (! 'L5 < L19'))\",\n",
" \"('L19 < L6' <-> (! 'L6 < L19'))\",\n",
" \"('L19 < L7' <-> (! 'L7 < L19'))\",\n",
" \"('L19 < L9' <-> (! 'L9 < L19'))\",\n",
" \"('L19 < [L0, L2, L13, L16]' <-> 'L19 < L0')\",\n",
" \"('L19 < [L0, L2, L13, L16]' <-> 'L19 < L13')\",\n",
" \"('L19 < [L0, L2, L13, L16]' <-> 'L19 < L16')\",\n",
" \"('L19 < [L0, L2, L13, L16]' <-> 'L19 < L2')\",\n",
" \"('L19 < [L1, L5, L6, L10, L14, L17]' <-> 'L19 < L1')\",\n",
" \"('L19 < [L1, L5, L6, L10, L14, L17]' <-> 'L19 < L10')\",\n",
" \"('L19 < [L1, L5, L6, L10, L14, L17]' <-> 'L19 < L14')\",\n",
" \"('L19 < [L1, L5, L6, L10, L14, L17]' <-> 'L19 < L17')\",\n",
" \"('L19 < [L1, L5, L6, L10, L14, L17]' <-> 'L19 < L5')\",\n",
" \"('L19 < [L1, L5, L6, L10, L14, L17]' <-> 'L19 < L6')\",\n",
" \"('L19 < [L1, L7, L14]' <-> 'L19 < L1')\",\n",
" \"('L19 < [L1, L7, L14]' <-> 'L19 < L14')\",\n",
" \"('L19 < [L1, L7, L14]' <-> 'L19 < L7')\",\n",
" \"('L19 < [L10, L13, L15]' <-> 'L19 < L10')\",\n",
" \"('L19 < [L10, L13, L15]' <-> 'L19 < L13')\",\n",
" \"('L19 < [L10, L13, L15]' <-> 'L19 < L15')\",\n",
" \"('L19 < [L3, L4, L10, L11, L18]' <-> 'L19 < L10')\",\n",
" \"('L19 < [L3, L4, L10, L11, L18]' <-> 'L19 < L11')\",\n",
" \"('L19 < [L3, L4, L10, L11, L18]' <-> 'L19 < L18')\",\n",
" \"('L19 < [L3, L4, L10, L11, L18]' <-> 'L19 < L3')\",\n",
" \"('L19 < [L3, L4, L10, L11, L18]' <-> 'L19 < L4')\",\n",
" \"('L19 < [L3, L5, L8]' <-> 'L19 < L3')\",\n",
" \"('L19 < [L3, L5, L8]' <-> 'L19 < L5')\",\n",
" \"('L19 < [L3, L5, L8]' <-> 'L19 < L8')\",\n",
" \"('L19 < [L4, L12, L14]' <-> 'L19 < L12')\",\n",
" \"('L19 < [L4, L12, L14]' <-> 'L19 < L14')\",\n",
" \"('L19 < [L4, L12, L14]' <-> 'L19 < L4')\",\n",
" \"('L19 < [L4, L6, L10, L16]' <-> 'L19 < L10')\",\n",
" \"('L19 < [L4, L6, L10, L16]' <-> 'L19 < L16')\",\n",
" \"('L19 < [L4, L6, L10, L16]' <-> 'L19 < L4')\",\n",
" \"('L19 < [L4, L6, L10, L16]' <-> 'L19 < L6')\",\n",
" \"('L19 < [L4, L7, L8, L13, L14, L18]' <-> 'L19 < L13')\",\n",
" \"('L19 < [L4, L7, L8, L13, L14, L18]' <-> 'L19 < L14')\",\n",
" \"('L19 < [L4, L7, L8, L13, L14, L18]' <-> 'L19 < L18')\",\n",
" \"('L19 < [L4, L7, L8, L13, L14, L18]' <-> 'L19 < L4')\",\n",
" \"('L19 < [L4, L7, L8, L13, L14, L18]' <-> 'L19 < L7')\",\n",
" \"('L19 < [L4, L7, L8, L13, L14, L18]' <-> 'L19 < L8')\",\n",
" \"('L19 < [L5, L10, L13]' <-> 'L19 < L10')\",\n",
" \"('L19 < [L5, L10, L13]' <-> 'L19 < L13')\",\n",
" \"('L19 < [L5, L10, L13]' <-> 'L19 < L5')\",\n",
" \"('L19 < [L8, L9, L12, L13]' <-> 'L19 < L12')\",\n",
" \"('L19 < [L8, L9, L12, L13]' <-> 'L19 < L13')\",\n",
" \"('L19 < [L8, L9, L12, L13]' <-> 'L19 < L8')\",\n",
" \"('L19 < [L8, L9, L12, L13]' <-> 'L19 < L9')\",\n",
" \"('L2 < L10' <-> (! 'L10 < L2'))\",\n",
" \"('L2 < L11' <-> (! 'L11 < L2'))\",\n",
" \"('L2 < L12' <-> (! 'L12 < L2'))\",\n",
" \"('L2 < L13' <-> (! 'L13 < L2'))\",\n",
" \"('L2 < L14' <-> (! 'L14 < L2'))\",\n",
" \"('L2 < L15' <-> (! 'L15 < L2'))\",\n",
" \"('L2 < L18' <-> (! 'L18 < L2'))\",\n",
" \"('L2 < L19' <-> (! 'L19 < L2'))\",\n",
" \"('L2 < L3' <-> (! 'L3 < L2'))\",\n",
" \"('L2 < L6' <-> (! 'L6 < L2'))\",\n",
" \"('L2 < L7' <-> (! 'L7 < L2'))\",\n",
" \"('L2 < L9' <-> (! 'L9 < L2'))\",\n",
" \"('L2 < [L3, L6, L7, L9, L19]' <-> 'L2 < L19')\",\n",
" \"('L2 < [L3, L6, L7, L9, L19]' <-> 'L2 < L3')\",\n",
" \"('L2 < [L3, L6, L7, L9, L19]' <-> 'L2 < L6')\",\n",
" \"('L2 < [L3, L6, L7, L9, L19]' <-> 'L2 < L7')\",\n",
" \"('L2 < [L3, L6, L7, L9, L19]' <-> 'L2 < L9')\",\n",
" \"('L3 < L10' <-> (! 'L10 < L3'))\",\n",
" \"('L3 < L11' <-> (! 'L11 < L3'))\",\n",
" \"('L3 < L12' <-> (! 'L12 < L3'))\",\n",
" \"('L3 < L13' <-> (! 'L13 < L3'))\",\n",
" \"('L3 < L14' <-> (! 'L14 < L3'))\",\n",
" \"('L3 < L15' <-> (! 'L15 < L3'))\",\n",
" \"('L3 < L16' <-> (! 'L16 < L3'))\",\n",
" \"('L3 < L17' <-> (! 'L17 < L3'))\",\n",
" \"('L3 < L18' <-> (! 'L18 < L3'))\",\n",
" \"('L3 < L4' <-> (! 'L4 < L3'))\",\n",
" \"('L3 < L5' <-> (! 'L5 < L3'))\",\n",
" \"('L3 < L6' <-> (! 'L6 < L3'))\",\n",
" \"('L3 < [L0, L2, L13, L16]' <-> 'L3 < L0')\",\n",
" \"('L3 < [L0, L2, L13, L16]' <-> 'L3 < L13')\",\n",
" \"('L3 < [L0, L2, L13, L16]' <-> 'L3 < L16')\",\n",
" \"('L3 < [L0, L2, L13, L16]' <-> 'L3 < L2')\",\n",
" \"('L3 < [L1, L5, L6, L10, L14, L17]' <-> 'L3 < L1')\",\n",
" \"('L3 < [L1, L5, L6, L10, L14, L17]' <-> 'L3 < L10')\",\n",
" \"('L3 < [L1, L5, L6, L10, L14, L17]' <-> 'L3 < L14')\",\n",
" \"('L3 < [L1, L5, L6, L10, L14, L17]' <-> 'L3 < L17')\",\n",
" \"('L3 < [L1, L5, L6, L10, L14, L17]' <-> 'L3 < L5')\",\n",
" \"('L3 < [L1, L5, L6, L10, L14, L17]' <-> 'L3 < L6')\",\n",
" \"('L3 < [L10, L13, L15]' <-> 'L3 < L10')\",\n",
" \"('L3 < [L10, L13, L15]' <-> 'L3 < L13')\",\n",
" \"('L3 < [L10, L13, L15]' <-> 'L3 < L15')\",\n",
" \"('L3 < [L4, L12, L14]' <-> 'L3 < L12')\",\n",
" \"('L3 < [L4, L12, L14]' <-> 'L3 < L14')\",\n",
" \"('L3 < [L4, L12, L14]' <-> 'L3 < L4')\",\n",
" \"('L3 < [L4, L6, L10, L16]' <-> 'L3 < L10')\",\n",
" \"('L3 < [L4, L6, L10, L16]' <-> 'L3 < L16')\",\n",
" \"('L3 < [L4, L6, L10, L16]' <-> 'L3 < L4')\",\n",
" \"('L3 < [L4, L6, L10, L16]' <-> 'L3 < L6')\",\n",
" \"('L3 < [L5, L10, L13]' <-> 'L3 < L10')\",\n",
" \"('L3 < [L5, L10, L13]' <-> 'L3 < L13')\",\n",
" \"('L3 < [L5, L10, L13]' <-> 'L3 < L5')\",\n",
" \"('L4 < L0' <-> (! 'L0 < L4'))\",\n",
" \"('L4 < L10' <-> (! 'L10 < L4'))\",\n",
" \"('L4 < L11' <-> (! 'L11 < L4'))\",\n",
" \"('L4 < L12' <-> (! 'L12 < L4'))\",\n",
" \"('L4 < L13' <-> (! 'L13 < L4'))\",\n",
" \"('L4 < L14' <-> (! 'L14 < L4'))\",\n",
" \"('L4 < L15' <-> (! 'L15 < L4'))\",\n",
" \"('L4 < L17' <-> (! 'L17 < L4'))\",\n",
" \"('L4 < L18' <-> (! 'L18 < L4'))\",\n",
" \"('L4 < L2' <-> (! 'L2 < L4'))\",\n",
" \"('L4 < L5' <-> (! 'L5 < L4'))\",\n",
" \"('L4 < L6' <-> (! 'L6 < L4'))\",\n",
" \"('L4 < L7' <-> (! 'L7 < L4'))\",\n",
" \"('L4 < L8' <-> (! 'L8 < L4'))\",\n",
" \"('L4 < L9' <-> (! 'L9 < L4'))\",\n",
" \"('L4 < [L1, L5, L6, L10, L14, L17]' <-> 'L4 < L1')\",\n",
" \"('L4 < [L1, L5, L6, L10, L14, L17]' <-> 'L4 < L10')\",\n",
" \"('L4 < [L1, L5, L6, L10, L14, L17]' <-> 'L4 < L14')\",\n",
" \"('L4 < [L1, L5, L6, L10, L14, L17]' <-> 'L4 < L17')\",\n",
" \"('L4 < [L1, L5, L6, L10, L14, L17]' <-> 'L4 < L5')\",\n",
" \"('L4 < [L1, L5, L6, L10, L14, L17]' <-> 'L4 < L6')\",\n",
" \"('L4 < [L1, L7, L14]' <-> 'L4 < L1')\",\n",
" \"('L4 < [L1, L7, L14]' <-> 'L4 < L14')\",\n",
" \"('L4 < [L1, L7, L14]' <-> 'L4 < L7')\",\n",
" \"('L4 < [L10, L13, L15]' <-> 'L4 < L10')\",\n",
" \"('L4 < [L10, L13, L15]' <-> 'L4 < L13')\",\n",
" \"('L4 < [L10, L13, L15]' <-> 'L4 < L15')\",\n",
" \"('L4 < [L5, L10, L13]' <-> 'L4 < L10')\",\n",
" \"('L4 < [L5, L10, L13]' <-> 'L4 < L13')\",\n",
" \"('L4 < [L5, L10, L13]' <-> 'L4 < L5')\",\n",
" \"('L4 < [L8, L9, L12, L13]' <-> 'L4 < L12')\",\n",
" \"('L4 < [L8, L9, L12, L13]' <-> 'L4 < L13')\",\n",
" \"('L4 < [L8, L9, L12, L13]' <-> 'L4 < L8')\",\n",
" \"('L4 < [L8, L9, L12, L13]' <-> 'L4 < L9')\",\n",
" \"('L5 < L0' <-> (! 'L0 < L5'))\",\n",
" \"('L5 < L10' <-> (! 'L10 < L5'))\",\n",
" \"('L5 < L11' <-> (! 'L11 < L5'))\",\n",
" \"('L5 < L12' <-> (! 'L12 < L5'))\",\n",
" \"('L5 < L13' <-> (! 'L13 < L5'))\",\n",
" \"('L5 < L14' <-> (! 'L14 < L5'))\",\n",
" \"('L5 < L15' <-> (! 'L15 < L5'))\",\n",
" \"('L5 < L16' <-> (! 'L16 < L5'))\",\n",
" \"('L5 < L18' <-> (! 'L18 < L5'))\",\n",
" \"('L5 < L2' <-> (! 'L2 < L5'))\",\n",
" \"('L5 < L6' <-> (! 'L6 < L5'))\",\n",
" \"('L5 < L7' <-> (! 'L7 < L5'))\",\n",
" \"('L5 < L8' <-> (! 'L8 < L5'))\",\n",
" \"('L5 < L9' <-> (! 'L9 < L5'))\",\n",
" \"('L5 < [L1, L7, L14]' <-> 'L5 < L1')\",\n",
" \"('L5 < [L1, L7, L14]' <-> 'L5 < L14')\",\n",
" \"('L5 < [L1, L7, L14]' <-> 'L5 < L7')\",\n",
" \"('L5 < [L10, L13, L15]' <-> 'L5 < L10')\",\n",
" \"('L5 < [L10, L13, L15]' <-> 'L5 < L13')\",\n",
" \"('L5 < [L10, L13, L15]' <-> 'L5 < L15')\",\n",
" \"('L5 < [L3, L4, L10, L11, L18]' <-> 'L5 < L10')\",\n",
" \"('L5 < [L3, L4, L10, L11, L18]' <-> 'L5 < L11')\",\n",
" \"('L5 < [L3, L4, L10, L11, L18]' <-> 'L5 < L18')\",\n",
" \"('L5 < [L3, L4, L10, L11, L18]' <-> 'L5 < L3')\",\n",
" \"('L5 < [L3, L4, L10, L11, L18]' <-> 'L5 < L4')\",\n",
" \"('L5 < [L4, L12, L14]' <-> 'L5 < L12')\",\n",
" \"('L5 < [L4, L12, L14]' <-> 'L5 < L14')\",\n",
" \"('L5 < [L4, L12, L14]' <-> 'L5 < L4')\",\n",
" \"('L5 < [L4, L6, L10, L16]' <-> 'L5 < L10')\",\n",
" \"('L5 < [L4, L6, L10, L16]' <-> 'L5 < L16')\",\n",
" \"('L5 < [L4, L6, L10, L16]' <-> 'L5 < L4')\",\n",
" \"('L5 < [L4, L6, L10, L16]' <-> 'L5 < L6')\",\n",
" \"('L5 < [L4, L7, L8, L13, L14, L18]' <-> 'L5 < L13')\",\n",
" \"('L5 < [L4, L7, L8, L13, L14, L18]' <-> 'L5 < L14')\",\n",
" \"('L5 < [L4, L7, L8, L13, L14, L18]' <-> 'L5 < L18')\",\n",
" \"('L5 < [L4, L7, L8, L13, L14, L18]' <-> 'L5 < L4')\",\n",
" \"('L5 < [L4, L7, L8, L13, L14, L18]' <-> 'L5 < L7')\",\n",
" \"('L5 < [L4, L7, L8, L13, L14, L18]' <-> 'L5 < L8')\",\n",
" \"('L5 < [L8, L9, L12, L13]' <-> 'L5 < L12')\",\n",
" \"('L5 < [L8, L9, L12, L13]' <-> 'L5 < L13')\",\n",
" \"('L5 < [L8, L9, L12, L13]' <-> 'L5 < L8')\",\n",
" \"('L5 < [L8, L9, L12, L13]' <-> 'L5 < L9')\",\n",
" \"('L6 < L10' <-> (! 'L10 < L6'))\",\n",
" \"('L6 < L12' <-> (! 'L12 < L6'))\",\n",
" \"('L6 < L13' <-> (! 'L13 < L6'))\",\n",
" \"('L6 < L14' <-> (! 'L14 < L6'))\",\n",
" \"('L6 < L15' <-> (! 'L15 < L6'))\",\n",
" \"('L6 < L16' <-> (! 'L16 < L6'))\",\n",
" \"('L6 < L18' <-> (! 'L18 < L6'))\",\n",
" \"('L6 < L8' <-> (! 'L8 < L6'))\",\n",
" \"('L6 < [L0, L2, L13, L16]' <-> 'L6 < L0')\",\n",
" \"('L6 < [L0, L2, L13, L16]' <-> 'L6 < L13')\",\n",
" \"('L6 < [L0, L2, L13, L16]' <-> 'L6 < L16')\",\n",
" \"('L6 < [L0, L2, L13, L16]' <-> 'L6 < L2')\",\n",
" \"('L6 < [L10, L13, L15]' <-> 'L6 < L10')\",\n",
" \"('L6 < [L10, L13, L15]' <-> 'L6 < L13')\",\n",
" \"('L6 < [L10, L13, L15]' <-> 'L6 < L15')\",\n",
" \"('L6 < [L3, L5, L8]' <-> 'L6 < L3')\",\n",
" \"('L6 < [L3, L5, L8]' <-> 'L6 < L5')\",\n",
" \"('L6 < [L3, L5, L8]' <-> 'L6 < L8')\",\n",
" \"('L6 < [L4, L12, L14]' <-> 'L6 < L12')\",\n",
" \"('L6 < [L4, L12, L14]' <-> 'L6 < L14')\",\n",
" \"('L6 < [L4, L12, L14]' <-> 'L6 < L4')\",\n",
" \"('L7 < L1' <-> (! 'L1 < L7'))\",\n",
" \"('L7 < L10' <-> (! 'L10 < L7'))\",\n",
" \"('L7 < L11' <-> (! 'L11 < L7'))\",\n",
" \"('L7 < L12' <-> (! 'L12 < L7'))\",\n",
" \"('L7 < L13' <-> (! 'L13 < L7'))\",\n",
" \"('L7 < L14' <-> (! 'L14 < L7'))\",\n",
" \"('L7 < L15' <-> (! 'L15 < L7'))\",\n",
" \"('L7 < L16' <-> (! 'L16 < L7'))\",\n",
" \"('L7 < L17' <-> (! 'L17 < L7'))\",\n",
" \"('L7 < L18' <-> (! 'L18 < L7'))\",\n",
" \"('L7 < L3' <-> (! 'L3 < L7'))\",\n",
" \"('L7 < L6' <-> (! 'L6 < L7'))\",\n",
" \"('L7 < L8' <-> (! 'L8 < L7'))\",\n",
" \"('L7 < L9' <-> (! 'L9 < L7'))\",\n",
" \"('L7 < [L0, L2, L13, L16]' <-> 'L7 < L0')\",\n",
" \"('L7 < [L0, L2, L13, L16]' <-> 'L7 < L13')\",\n",
" \"('L7 < [L0, L2, L13, L16]' <-> 'L7 < L16')\",\n",
" \"('L7 < [L0, L2, L13, L16]' <-> 'L7 < L2')\",\n",
" \"('L7 < [L0, L9]' <-> 'L7 < L0')\",\n",
" \"('L7 < [L0, L9]' <-> 'L7 < L9')\",\n",
" \"('L7 < [L1, L5, L6, L10, L14, L17]' <-> 'L7 < L1')\",\n",
" \"('L7 < [L1, L5, L6, L10, L14, L17]' <-> 'L7 < L10')\",\n",
" \"('L7 < [L1, L5, L6, L10, L14, L17]' <-> 'L7 < L14')\",\n",
" \"('L7 < [L1, L5, L6, L10, L14, L17]' <-> 'L7 < L17')\",\n",
" \"('L7 < [L1, L5, L6, L10, L14, L17]' <-> 'L7 < L5')\",\n",
" \"('L7 < [L1, L5, L6, L10, L14, L17]' <-> 'L7 < L6')\",\n",
" \"('L7 < [L10, L13, L15]' <-> 'L7 < L10')\",\n",
" \"('L7 < [L10, L13, L15]' <-> 'L7 < L13')\",\n",
" \"('L7 < [L10, L13, L15]' <-> 'L7 < L15')\",\n",
" \"('L7 < [L2, L8, L9]' <-> 'L7 < L2')\",\n",
" \"('L7 < [L2, L8, L9]' <-> 'L7 < L8')\",\n",
" \"('L7 < [L2, L8, L9]' <-> 'L7 < L9')\",\n",
" \"('L7 < [L3, L4, L10, L11, L18]' <-> 'L7 < L10')\",\n",
" \"('L7 < [L3, L4, L10, L11, L18]' <-> 'L7 < L11')\",\n",
" \"('L7 < [L3, L4, L10, L11, L18]' <-> 'L7 < L18')\",\n",
" \"('L7 < [L3, L4, L10, L11, L18]' <-> 'L7 < L3')\",\n",
" \"('L7 < [L3, L4, L10, L11, L18]' <-> 'L7 < L4')\",\n",
" \"('L7 < [L3, L5, L8]' <-> 'L7 < L3')\",\n",
" \"('L7 < [L3, L5, L8]' <-> 'L7 < L5')\",\n",
" \"('L7 < [L3, L5, L8]' <-> 'L7 < L8')\",\n",
" \"('L7 < [L4, L12, L14]' <-> 'L7 < L12')\",\n",
" \"('L7 < [L4, L12, L14]' <-> 'L7 < L14')\",\n",
" \"('L7 < [L4, L12, L14]' <-> 'L7 < L4')\",\n",
" \"('L7 < [L4, L6, L10, L16]' <-> 'L7 < L10')\",\n",
" \"('L7 < [L4, L6, L10, L16]' <-> 'L7 < L16')\",\n",
" \"('L7 < [L4, L6, L10, L16]' <-> 'L7 < L4')\",\n",
" \"('L7 < [L4, L6, L10, L16]' <-> 'L7 < L6')\",\n",
" \"('L7 < [L5, L10, L13]' <-> 'L7 < L10')\",\n",
" \"('L7 < [L5, L10, L13]' <-> 'L7 < L13')\",\n",
" \"('L7 < [L5, L10, L13]' <-> 'L7 < L5')\",\n",
" \"('L7 < [L8, L9, L12, L13]' <-> 'L7 < L12')\",\n",
" \"('L7 < [L8, L9, L12, L13]' <-> 'L7 < L13')\",\n",
" \"('L7 < [L8, L9, L12, L13]' <-> 'L7 < L8')\",\n",
" \"('L7 < [L8, L9, L12, L13]' <-> 'L7 < L9')\",\n",
" \"('L8 < L1' <-> (! 'L1 < L8'))\",\n",
" \"('L8 < L10' <-> (! 'L10 < L8'))\",\n",
" \"('L8 < L11' <-> (! 'L11 < L8'))\",\n",
" \"('L8 < L12' <-> (! 'L12 < L8'))\",\n",
" \"('L8 < L13' <-> (! 'L13 < L8'))\",\n",
" \"('L8 < L14' <-> (! 'L14 < L8'))\",\n",
" \"('L8 < L15' <-> (! 'L15 < L8'))\",\n",
" \"('L8 < L16' <-> (! 'L16 < L8'))\",\n",
" \"('L8 < L17' <-> (! 'L17 < L8'))\",\n",
" \"('L8 < L18' <-> (! 'L18 < L8'))\",\n",
" \"('L8 < L19' <-> (! 'L19 < L8'))\",\n",
" \"('L8 < L2' <-> (! 'L2 < L8'))\",\n",
" \"('L8 < L3' <-> (! 'L3 < L8'))\",\n",
" \"('L8 < L9' <-> (! 'L9 < L8'))\",\n",
" \"('L8 < [L0, L2, L13, L16]' <-> 'L8 < L0')\",\n",
" \"('L8 < [L0, L2, L13, L16]' <-> 'L8 < L13')\",\n",
" \"('L8 < [L0, L2, L13, L16]' <-> 'L8 < L16')\",\n",
" \"('L8 < [L0, L2, L13, L16]' <-> 'L8 < L2')\",\n",
" \"('L8 < [L1, L5, L6, L10, L14, L17]' <-> 'L8 < L1')\",\n",
" \"('L8 < [L1, L5, L6, L10, L14, L17]' <-> 'L8 < L10')\",\n",
" \"('L8 < [L1, L5, L6, L10, L14, L17]' <-> 'L8 < L14')\",\n",
" \"('L8 < [L1, L5, L6, L10, L14, L17]' <-> 'L8 < L17')\",\n",
" \"('L8 < [L1, L5, L6, L10, L14, L17]' <-> 'L8 < L5')\",\n",
" \"('L8 < [L1, L5, L6, L10, L14, L17]' <-> 'L8 < L6')\",\n",
" \"('L8 < [L1, L7, L14]' <-> 'L8 < L1')\",\n",
" \"('L8 < [L1, L7, L14]' <-> 'L8 < L14')\",\n",
" \"('L8 < [L1, L7, L14]' <-> 'L8 < L7')\",\n",
" \"('L8 < [L10, L13, L15]' <-> 'L8 < L10')\",\n",
" \"('L8 < [L10, L13, L15]' <-> 'L8 < L13')\",\n",
" \"('L8 < [L10, L13, L15]' <-> 'L8 < L15')\",\n",
" \"('L8 < [L3, L4, L10, L11, L18]' <-> 'L8 < L10')\",\n",
" \"('L8 < [L3, L4, L10, L11, L18]' <-> 'L8 < L11')\",\n",
" \"('L8 < [L3, L4, L10, L11, L18]' <-> 'L8 < L18')\",\n",
" \"('L8 < [L3, L4, L10, L11, L18]' <-> 'L8 < L3')\",\n",
" \"('L8 < [L3, L4, L10, L11, L18]' <-> 'L8 < L4')\",\n",
" \"('L8 < [L3, L6, L7, L9, L19]' <-> 'L8 < L19')\",\n",
" \"('L8 < [L3, L6, L7, L9, L19]' <-> 'L8 < L3')\",\n",
" \"('L8 < [L3, L6, L7, L9, L19]' <-> 'L8 < L6')\",\n",
" \"('L8 < [L3, L6, L7, L9, L19]' <-> 'L8 < L7')\",\n",
" \"('L8 < [L3, L6, L7, L9, L19]' <-> 'L8 < L9')\",\n",
" \"('L8 < [L4, L12, L14]' <-> 'L8 < L12')\",\n",
" \"('L8 < [L4, L12, L14]' <-> 'L8 < L14')\",\n",
" \"('L8 < [L4, L12, L14]' <-> 'L8 < L4')\",\n",
" \"('L8 < [L4, L6, L10, L16]' <-> 'L8 < L10')\",\n",
" \"('L8 < [L4, L6, L10, L16]' <-> 'L8 < L16')\",\n",
" \"('L8 < [L4, L6, L10, L16]' <-> 'L8 < L4')\",\n",
" \"('L8 < [L4, L6, L10, L16]' <-> 'L8 < L6')\",\n",
" \"('L8 < [L5, L10, L13]' <-> 'L8 < L10')\",\n",
" \"('L8 < [L5, L10, L13]' <-> 'L8 < L13')\",\n",
" \"('L8 < [L5, L10, L13]' <-> 'L8 < L5')\",\n",
" \"('L9 < L1' <-> (! 'L1 < L9'))\",\n",
" \"('L9 < L10' <-> (! 'L10 < L9'))\",\n",
" \"('L9 < L11' <-> (! 'L11 < L9'))\",\n",
" \"('L9 < L12' <-> (! 'L12 < L9'))\",\n",
" \"('L9 < L13' <-> (! 'L13 < L9'))\",\n",
" \"('L9 < L14' <-> (! 'L14 < L9'))\",\n",
" \"('L9 < L15' <-> (! 'L15 < L9'))\",\n",
" \"('L9 < L16' <-> (! 'L16 < L9'))\",\n",
" \"('L9 < L17' <-> (! 'L17 < L9'))\",\n",
" \"('L9 < L18' <-> (! 'L18 < L9'))\",\n",
" \"('L9 < L3' <-> (! 'L3 < L9'))\",\n",
" \"('L9 < L6' <-> (! 'L6 < L9'))\",\n",
" \"('L9 < [L0, L2, L13, L16]' <-> 'L9 < L0')\",\n",
" \"('L9 < [L0, L2, L13, L16]' <-> 'L9 < L13')\",\n",
" \"('L9 < [L0, L2, L13, L16]' <-> 'L9 < L16')\",\n",
" \"('L9 < [L0, L2, L13, L16]' <-> 'L9 < L2')\",\n",
" \"('L9 < [L1, L5, L6, L10, L14, L17]' <-> 'L9 < L1')\",\n",
" \"('L9 < [L1, L5, L6, L10, L14, L17]' <-> 'L9 < L10')\",\n",
" \"('L9 < [L1, L5, L6, L10, L14, L17]' <-> 'L9 < L14')\",\n",
" \"('L9 < [L1, L5, L6, L10, L14, L17]' <-> 'L9 < L17')\",\n",
" \"('L9 < [L1, L5, L6, L10, L14, L17]' <-> 'L9 < L5')\",\n",
" \"('L9 < [L1, L5, L6, L10, L14, L17]' <-> 'L9 < L6')\",\n",
" \"('L9 < [L1, L7, L14]' <-> 'L9 < L1')\",\n",
" \"('L9 < [L1, L7, L14]' <-> 'L9 < L14')\",\n",
" \"('L9 < [L1, L7, L14]' <-> 'L9 < L7')\",\n",
" \"('L9 < [L10, L13, L15]' <-> 'L9 < L10')\",\n",
" \"('L9 < [L10, L13, L15]' <-> 'L9 < L13')\",\n",
" \"('L9 < [L10, L13, L15]' <-> 'L9 < L15')\",\n",
" \"('L9 < [L3, L4, L10, L11, L18]' <-> 'L9 < L10')\",\n",
" \"('L9 < [L3, L4, L10, L11, L18]' <-> 'L9 < L11')\",\n",
" \"('L9 < [L3, L4, L10, L11, L18]' <-> 'L9 < L18')\",\n",
" \"('L9 < [L3, L4, L10, L11, L18]' <-> 'L9 < L3')\",\n",
" \"('L9 < [L3, L4, L10, L11, L18]' <-> 'L9 < L4')\",\n",
" \"('L9 < [L3, L5, L8]' <-> 'L9 < L3')\",\n",
" \"('L9 < [L3, L5, L8]' <-> 'L9 < L5')\",\n",
" \"('L9 < [L3, L5, L8]' <-> 'L9 < L8')\",\n",
" \"('L9 < [L4, L12, L14]' <-> 'L9 < L12')\",\n",
" \"('L9 < [L4, L12, L14]' <-> 'L9 < L14')\",\n",
" \"('L9 < [L4, L12, L14]' <-> 'L9 < L4')\",\n",
" \"('L9 < [L4, L6, L10, L16]' <-> 'L9 < L10')\",\n",
" \"('L9 < [L4, L6, L10, L16]' <-> 'L9 < L16')\",\n",
" \"('L9 < [L4, L6, L10, L16]' <-> 'L9 < L4')\",\n",
" \"('L9 < [L4, L6, L10, L16]' <-> 'L9 < L6')\",\n",
" \"('L9 < [L5, L10, L13]' <-> 'L9 < L10')\",\n",
" \"('L9 < [L5, L10, L13]' <-> 'L9 < L13')\",\n",
" \"('L9 < [L5, L10, L13]' <-> 'L9 < L5')\",\n",
" \"(('L0 < L10' & 'L10 < L3') -> 'L0 < L3')\",\n",
" \"(('L0 < L11' & 'L11 < L7') -> 'L0 < L7')\",\n",
" \"(('L0 < L12' & 'L12 < L19') -> 'L0 < L19')\",\n",
" \"(('L0 < L13' & 'L13 < L17') -> 'L0 < L17')\",\n",
" \"(('L0 < L13' & 'L13 < L7') -> 'L0 < L7')\",\n",
" \"(('L0 < L14' & 'L14 < L17') -> 'L0 < L17')\",\n",
" \"(('L0 < L14' & 'L14 < L19') -> 'L0 < L19')\",\n",
" \"(('L0 < L14' & 'L14 < L3') -> 'L0 < L3')\",\n",
" \"(('L0 < L14' & 'L14 < L7') -> 'L0 < L7')\",\n",
" \"(('L0 < L15' & 'L15 < L17') -> 'L0 < L17')\",\n",
" \"(('L0 < L15' & 'L15 < L19') -> 'L0 < L19')\",\n",
" \"(('L0 < L17' & 'L17 < L19') -> 'L0 < L19')\",\n",
" \"(('L0 < L17' & 'L17 < L2') -> 'L0 < L2')\",\n",
" \"(('L0 < L17' & 'L17 < L5') -> 'L0 < L5')\",\n",
" \"(('L0 < L18' & 'L18 < L17') -> 'L0 < L17')\",\n",
" \"(('L0 < L18' & 'L18 < L19') -> 'L0 < L19')\",\n",
" \"(('L0 < L18' & 'L18 < L7') -> 'L0 < L7')\",\n",
" \"(('L0 < L19' & 'L19 < L10') -> 'L0 < L10')\",\n",
" \"(('L0 < L19' & 'L19 < L16') -> 'L0 < L16')\",\n",
" \"(('L0 < L19' & 'L19 < L2') -> 'L0 < L2')\",\n",
" \"(('L0 < L19' & 'L19 < L3') -> 'L0 < L3')\",\n",
" \"(('L0 < L19' & 'L19 < L4') -> 'L0 < L4')\",\n",
" \"(('L0 < L19' & 'L19 < L5') -> 'L0 < L5')\",\n",
" \"(('L0 < L19' & 'L19 < L7') -> 'L0 < L7')\",\n",
" \"(('L0 < L6' & 'L6 < L14') -> 'L0 < L14')\",\n",
" \"(('L0 < L6' & 'L6 < L15') -> 'L0 < L15')\",\n",
" \"(('L0 < L6' & 'L6 < L7') -> 'L0 < L7')\",\n",
" \"(('L0 < L8' & 'L8 < L1') -> 'L0 < L1')\",\n",
" \"(('L0 < L8' & 'L8 < L11') -> 'L0 < L11')\",\n",
" \"(('L0 < L8' & 'L8 < L14') -> 'L0 < L14')\",\n",
" \"(('L0 < L8' & 'L8 < L16') -> 'L0 < L16')\",\n",
" \"(('L0 < L8' & 'L8 < L17') -> 'L0 < L17')\",\n",
" \"(('L0 < L8' & 'L8 < L18') -> 'L0 < L18')\",\n",
" \"(('L0 < L8' & 'L8 < L7') -> 'L0 < L7')\",\n",
" \"(('L0 < L9' & 'L9 < L10') -> 'L0 < L10')\",\n",
" \"(('L0 < L9' & 'L9 < L11') -> 'L0 < L11')\",\n",
" \"(('L0 < L9' & 'L9 < L15') -> 'L0 < L15')\",\n",
" \"(('L0 < L9' & 'L9 < L17') -> 'L0 < L17')\",\n",
" \"(('L0 < L9' & 'L9 < L18') -> 'L0 < L18')\",\n",
" \"(('L0 < L9' & 'L9 < L19') -> 'L0 < L19')\",\n",
" \"(('L0 < L9' & 'L9 < L2') -> 'L0 < L2')\",\n",
" \"(('L0 < L9' & 'L9 < L3') -> 'L0 < L3')\",\n",
" \"(('L0 < L9' & 'L9 < L5') -> 'L0 < L5')\",\n",
" \"(('L0 < L9' & 'L9 < L6') -> 'L0 < L6')\",\n",
" \"(('L0 < L9' & 'L9 < L7') -> 'L0 < L7')\",\n",
" \"(('L1 < L10' & 'L11 < L1') -> 'L11 < L10')\",\n",
" \"(('L1 < L10' & 'L14 < L1') -> 'L14 < L10')\",\n",
" \"(('L1 < L10' & 'L15 < L1') -> 'L15 < L10')\",\n",
" \"(('L1 < L10' & 'L16 < L1') -> 'L16 < L10')\",\n",
" \"(('L1 < L10' & 'L17 < L1') -> 'L17 < L10')\",\n",
" \"(('L1 < L10' & 'L18 < L1') -> 'L18 < L10')\",\n",
" \"(('L1 < L10' & 'L3 < L1') -> 'L3 < L10')\",\n",
" \"(('L1 < L10' & 'L4 < L1') -> 'L4 < L10')\",\n",
" \"(('L1 < L10' & 'L6 < L1') -> 'L6 < L10')\",\n",
" \"(('L1 < L10' & 'L8 < L1') -> 'L8 < L10')\",\n",
" \"(('L1 < L11' & 'L11 < L15') -> 'L1 < L15')\",\n",
" \"(('L1 < L11' & 'L11 < L18') -> 'L1 < L18')\",\n",
" \"(('L1 < L11' & 'L11 < L6') -> 'L1 < L6')\",\n",
" \"(('L1 < L11' & 'L11 < L9') -> 'L1 < L9')\",\n",
" \"(('L1 < L11' & 'L5 < L1') -> 'L5 < L11')\",\n",
" \"(('L1 < L12' & 'L5 < L1') -> 'L5 < L12')\",\n",
" \"(('L1 < L13' & 'L10 < L1') -> 'L10 < L13')\",\n",
" \"(('L1 < L13' & 'L11 < L1') -> 'L11 < L13')\",\n",
" \"(('L1 < L13' & 'L13 < L12') -> 'L1 < L12')\",\n",
" \"(('L1 < L13' & 'L13 < L15') -> 'L1 < L15')\",\n",
" \"(('L1 < L13' & 'L13 < L18') -> 'L1 < L18')\",\n",
" \"(('L1 < L13' & 'L13 < L6') -> 'L1 < L6')\",\n",
" \"(('L1 < L13' & 'L13 < L8') -> 'L1 < L8')\",\n",
" \"(('L1 < L13' & 'L13 < L9') -> 'L1 < L9')\",\n",
" \"(('L1 < L13' & 'L14 < L1') -> 'L14 < L13')\",\n",
" \"(('L1 < L13' & 'L16 < L1') -> 'L16 < L13')\",\n",
" \"(('L1 < L13' & 'L3 < L1') -> 'L3 < L13')\",\n",
" \"(('L1 < L13' & 'L5 < L1') -> 'L5 < L13')\",\n",
" \"(('L1 < L13' & 'L7 < L1') -> 'L7 < L13')\",\n",
" \"(('L1 < L14' & 'L10 < L1') -> 'L10 < L14')\",\n",
" \"(('L1 < L14' & 'L11 < L1') -> 'L11 < L14')\",\n",
" \"(('L1 < L14' & 'L14 < L8') -> 'L1 < L8')\",\n",
" \"(('L1 < L14' & 'L14 < L9') -> 'L1 < L9')\",\n",
" \"(('L1 < L14' & 'L16 < L1') -> 'L16 < L14')\",\n",
" \"(('L1 < L14' & 'L3 < L1') -> 'L3 < L14')\",\n",
" \"(('L1 < L14' & 'L5 < L1') -> 'L5 < L14')\",\n",
" \"(('L1 < L14' & 'L7 < L1') -> 'L7 < L14')\",\n",
" \"(('L1 < L15' & 'L15 < L9') -> 'L1 < L9')\",\n",
" \"(('L1 < L15' & 'L5 < L1') -> 'L5 < L15')\",\n",
" \"(('L1 < L15' & 'L6 < L1') -> 'L6 < L15')\",\n",
" \"(('L1 < L15' & 'L8 < L1') -> 'L8 < L15')\",\n",
" \"(('L1 < L16' & 'L10 < L1') -> 'L10 < L16')\",\n",
" \"(('L1 < L16' & 'L11 < L1') -> 'L11 < L16')\",\n",
" \"(('L1 < L16' & 'L13 < L1') -> 'L13 < L16')\",\n",
" \"(('L1 < L16' & 'L14 < L1') -> 'L14 < L16')\",\n",
" \"(('L1 < L16' & 'L15 < L1') -> 'L15 < L16')\",\n",
" \"(('L1 < L16' & 'L16 < L7') -> 'L1 < L7')\",\n",
" \"(('L1 < L16' & 'L17 < L1') -> 'L17 < L16')\",\n",
" \"(('L1 < L16' & 'L18 < L1') -> 'L18 < L16')\",\n",
" \"(('L1 < L16' & 'L3 < L1') -> 'L3 < L16')\",\n",
" \"(('L1 < L16' & 'L4 < L1') -> 'L4 < L16')\",\n",
" \"(('L1 < L16' & 'L6 < L1') -> 'L6 < L16')\",\n",
" \"(('L1 < L16' & 'L8 < L1') -> 'L8 < L16')\",\n",
" \"(('L1 < L16' & 'L9 < L1') -> 'L9 < L16')\",\n",
" \"(('L1 < L17' & 'L5 < L1') -> 'L5 < L17')\",\n",
" \"(('L1 < L18' & 'L15 < L1') -> 'L15 < L18')\",\n",
" \"(('L1 < L18' & 'L18 < L12') -> 'L1 < L12')\",\n",
" \"(('L1 < L18' & 'L18 < L9') -> 'L1 < L9')\",\n",
" \"(('L1 < L18' & 'L5 < L1') -> 'L5 < L18')\",\n",
" \"(('L1 < L19' & 'L5 < L1') -> 'L5 < L19')\",\n",
" \"(('L1 < L2' & 'L2 < L9') -> 'L1 < L9')\",\n",
" \"(('L1 < L3' & 'L0 < L1') -> 'L0 < L3')\",\n",
" \"(('L1 < L3' & 'L10 < L1') -> 'L10 < L3')\",\n",
" \"(('L1 < L3' & 'L11 < L1') -> 'L11 < L3')\",\n",
" \"(('L1 < L3' & 'L13 < L1') -> 'L13 < L3')\",\n",
" \"(('L1 < L3' & 'L14 < L1') -> 'L14 < L3')\",\n",
" \"(('L1 < L3' & 'L15 < L1') -> 'L15 < L3')\",\n",
" \"(('L1 < L3' & 'L16 < L1') -> 'L16 < L3')\",\n",
" \"(('L1 < L3' & 'L17 < L1') -> 'L17 < L3')\",\n",
" \"(('L1 < L3' & 'L18 < L1') -> 'L18 < L3')\",\n",
" \"(('L1 < L3' & 'L2 < L1') -> 'L2 < L3')\",\n",
" \"(('L1 < L3' & 'L4 < L1') -> 'L4 < L3')\",\n",
" \"(('L1 < L3' & 'L6 < L1') -> 'L6 < L3')\",\n",
" \"(('L1 < L3' & 'L8 < L1') -> 'L8 < L3')\",\n",
" \"(('L1 < L3' & 'L9 < L1') -> 'L9 < L3')\",\n",
" \"(('L1 < L4' & 'L10 < L1') -> 'L10 < L4')\",\n",
" \"(('L1 < L4' & 'L16 < L1') -> 'L16 < L4')\",\n",
" \"(('L1 < L4' & 'L3 < L1') -> 'L3 < L4')\",\n",
" \"(('L1 < L4' & 'L4 < L11') -> 'L1 < L11')\",\n",
" \"(('L1 < L4' & 'L4 < L12') -> 'L1 < L12')\",\n",
" \"(('L1 < L4' & 'L4 < L13') -> 'L1 < L13')\",\n",
" \"(('L1 < L4' & 'L4 < L14') -> 'L1 < L14')\",\n",
" \"(('L1 < L4' & 'L4 < L15') -> 'L1 < L15')\",\n",
" \"(('L1 < L4' & 'L4 < L17') -> 'L1 < L17')\",\n",
" \"(('L1 < L4' & 'L4 < L18') -> 'L1 < L18')\",\n",
" \"(('L1 < L4' & 'L4 < L19') -> 'L1 < L19')\",\n",
" \"(('L1 < L4' & 'L4 < L6') -> 'L1 < L6')\",\n",
" \"(('L1 < L4' & 'L4 < L8') -> 'L1 < L8')\",\n",
" \"(('L1 < L4' & 'L4 < L9') -> 'L1 < L9')\",\n",
" \"(('L1 < L4' & 'L5 < L1') -> 'L5 < L4')\",\n",
" \"(('L1 < L4' & 'L7 < L1') -> 'L7 < L4')\",\n",
" \"(('L1 < L5' & 'L17 < L1') -> 'L17 < L5')\",\n",
" \"(('L1 < L5' & 'L4 < L1') -> 'L4 < L5')\",\n",
" \"(('L1 < L5' & 'L8 < L1') -> 'L8 < L5')\",\n",
" \"(('L1 < L6' & 'L15 < L1') -> 'L15 < L6')\",\n",
" \"(('L1 < L6' & 'L5 < L1') -> 'L5 < L6')\",\n",
" \"(('L1 < L6' & 'L6 < L0') -> 'L1 < L0')\",\n",
" \"(('L1 < L6' & 'L6 < L15') -> 'L1 < L15')\",\n",
" \"(('L1 < L6' & 'L6 < L18') -> 'L1 < L18')\",\n",
" \"(('L1 < L6' & 'L6 < L9') -> 'L1 < L9')\",\n",
" \"(('L1 < L7' & 'L0 < L1') -> 'L0 < L7')\",\n",
" \"(('L1 < L7' & 'L11 < L1') -> 'L11 < L7')\",\n",
" \"(('L1 < L7' & 'L13 < L1') -> 'L13 < L7')\",\n",
" \"(('L1 < L7' & 'L14 < L1') -> 'L14 < L7')\",\n",
" \"(('L1 < L7' & 'L15 < L1') -> 'L15 < L7')\",\n",
" \"(('L1 < L7' & 'L17 < L1') -> 'L17 < L7')\",\n",
" \"(('L1 < L7' & 'L18 < L1') -> 'L18 < L7')\",\n",
" \"(('L1 < L7' & 'L2 < L1') -> 'L2 < L7')\",\n",
" \"(('L1 < L7' & 'L4 < L1') -> 'L4 < L7')\",\n",
" \"(('L1 < L7' & 'L6 < L1') -> 'L6 < L7')\",\n",
" \"(('L1 < L7' & 'L7 < L10') -> 'L1 < L10')\",\n",
" \"(('L1 < L7' & 'L7 < L16') -> 'L1 < L16')\",\n",
" \"(('L1 < L7' & 'L7 < L3') -> 'L1 < L3')\",\n",
" \"(('L1 < L7' & 'L7 < L5') -> 'L1 < L5')\",\n",
" \"(('L1 < L7' & 'L8 < L1') -> 'L8 < L7')\",\n",
" \"(('L1 < L7' & 'L9 < L1') -> 'L9 < L7')\",\n",
" \"(('L1 < L8' & 'L5 < L1') -> 'L5 < L8')\",\n",
" \"(('L1 < L8' & 'L8 < L18') -> 'L1 < L18')\",\n",
" \"(('L1 < L9' & 'L10 < L1') -> 'L10 < L9')\",\n",
" \"(('L1 < L9' & 'L16 < L1') -> 'L16 < L9')\",\n",
" \"(('L1 < L9' & 'L3 < L1') -> 'L3 < L9')\",\n",
" \"(('L1 < L9' & 'L5 < L1') -> 'L5 < L9')\",\n",
" \"(('L1 < L9' & 'L7 < L1') -> 'L7 < L9')\",\n",
" \"(('L1 < L9' & 'L9 < L0') -> 'L1 < L0')\",\n",
" \"(('L10 < L0' & 'L3 < L10') -> 'L3 < L0')\",\n",
" \"(('L10 < L1' & 'L1 < L11') -> 'L10 < L11')\",\n",
" \"(('L10 < L1' & 'L1 < L12') -> 'L10 < L12')\",\n",
" \"(('L10 < L1' & 'L1 < L15') -> 'L10 < L15')\",\n",
" \"(('L10 < L1' & 'L1 < L17') -> 'L10 < L17')\",\n",
" \"(('L10 < L1' & 'L1 < L18') -> 'L10 < L18')\",\n",
" \"(('L10 < L1' & 'L1 < L19') -> 'L10 < L19')\",\n",
" \"(('L10 < L1' & 'L1 < L6') -> 'L10 < L6')\",\n",
" \"(('L10 < L1' & 'L1 < L8') -> 'L10 < L8')\",\n",
" \"(('L10 < L11' & 'L11 < L9') -> 'L10 < L9')\",\n",
" \"(('L10 < L12' & 'L12 < L3') -> 'L10 < L3')\",\n",
" \"(('L10 < L12' & 'L3 < L10') -> 'L3 < L12')\",\n",
" \"(('L10 < L13' & 'L13 < L12') -> 'L10 < L12')\",\n",
" \"(('L10 < L13' & 'L13 < L14') -> 'L10 < L14')\",\n",
" \"(('L10 < L13' & 'L13 < L15') -> 'L10 < L15')\",\n",
" \"(('L10 < L13' & 'L13 < L3') -> 'L10 < L3')\",\n",
" \"(('L10 < L13' & 'L13 < L6') -> 'L10 < L6')\",\n",
" \"(('L10 < L13' & 'L13 < L8') -> 'L10 < L8')\",\n",
" \"(('L10 < L13' & 'L13 < L9') -> 'L10 < L9')\",\n",
" \"(('L10 < L14' & 'L14 < L3') -> 'L10 < L3')\",\n",
" \"(('L10 < L14' & 'L14 < L8') -> 'L10 < L8')\",\n",
" \"(('L10 < L15' & 'L15 < L12') -> 'L10 < L12')\",\n",
" \"(('L10 < L15' & 'L15 < L6') -> 'L10 < L6')\",\n",
" \"(('L10 < L15' & 'L15 < L8') -> 'L10 < L8')\",\n",
" \"(('L10 < L15' & 'L15 < L9') -> 'L10 < L9')\",\n",
" \"(('L10 < L15' & 'L3 < L10') -> 'L3 < L15')\",\n",
" \"(('L10 < L17' & 'L17 < L0') -> 'L10 < L0')\",\n",
" \"(('L10 < L17' & 'L17 < L13') -> 'L10 < L13')\",\n",
" \"(('L10 < L17' & 'L17 < L14') -> 'L10 < L14')\",\n",
" \"(('L10 < L17' & 'L17 < L15') -> 'L10 < L15')\",\n",
" \"(('L10 < L17' & 'L17 < L18') -> 'L10 < L18')\",\n",
" \"(('L10 < L17' & 'L17 < L3') -> 'L10 < L3')\",\n",
" \"(('L10 < L17' & 'L17 < L6') -> 'L10 < L6')\",\n",
" \"(('L10 < L17' & 'L17 < L8') -> 'L10 < L8')\",\n",
" \"(('L10 < L18' & 'L18 < L6') -> 'L10 < L6')\",\n",
" \"(('L10 < L19' & 'L19 < L0') -> 'L10 < L0')\",\n",
" \"(('L10 < L19' & 'L19 < L11') -> 'L10 < L11')\",\n",
" \"(('L10 < L19' & 'L19 < L12') -> 'L10 < L12')\",\n",
" \"(('L10 < L19' & 'L19 < L13') -> 'L10 < L13')\",\n",
" \"(('L10 < L19' & 'L19 < L14') -> 'L10 < L14')\",\n",
" \"(('L10 < L19' & 'L19 < L15') -> 'L10 < L15')\",\n",
" \"(('L10 < L19' & 'L19 < L17') -> 'L10 < L17')\",\n",
" \"(('L10 < L19' & 'L19 < L18') -> 'L10 < L18')\",\n",
" \"(('L10 < L19' & 'L19 < L3') -> 'L10 < L3')\",\n",
" \"(('L10 < L19' & 'L19 < L6') -> 'L10 < L6')\",\n",
" \"(('L10 < L19' & 'L19 < L8') -> 'L10 < L8')\",\n",
" \"(('L10 < L19' & 'L19 < L9') -> 'L10 < L9')\",\n",
" \"(('L10 < L2' & 'L2 < L17') -> 'L10 < L17')\",\n",
" \"(('L10 < L2' & 'L2 < L9') -> 'L10 < L9')\",\n",
" \"(('L10 < L5' & 'L5 < L1') -> 'L10 < L1')\",\n",
" \"(('L10 < L5' & 'L5 < L13') -> 'L10 < L13')\",\n",
" \"(('L10 < L5' & 'L5 < L15') -> 'L10 < L15')\",\n",
" \"(('L10 < L5' & 'L5 < L17') -> 'L10 < L17')\",\n",
" \"(('L10 < L5' & 'L5 < L4') -> 'L10 < L4')\",\n",
" \"(('L10 < L5' & 'L5 < L6') -> 'L10 < L6')\",\n",
" \"(('L10 < L5' & 'L5 < L7') -> 'L10 < L7')\",\n",
" \"(('L10 < L5' & 'L5 < L9') -> 'L10 < L9')\",\n",
" \"(('L10 < L6' & 'L3 < L10') -> 'L3 < L6')\",\n",
" \"(('L10 < L7' & 'L7 < L15') -> 'L10 < L15')\",\n",
" \"(('L10 < L7' & 'L7 < L3') -> 'L10 < L3')\",\n",
" \"(('L10 < L8' & 'L3 < L10') -> 'L3 < L8')\",\n",
" \"(('L10 < L8' & 'L8 < L0') -> 'L10 < L0')\",\n",
" \"(('L10 < L9' & 'L3 < L10') -> 'L3 < L9')\",\n",
" \"(('L11 < L0' & 'L7 < L11') -> 'L7 < L0')\",\n",
" \"(('L11 < L1' & 'L1 < L5') -> 'L11 < L5')\",\n",
" \"(('L11 < L1' & 'L15 < L11') -> 'L15 < L1')\",\n",
" \"(('L11 < L1' & 'L6 < L11') -> 'L6 < L1')\",\n",
" \"(('L11 < L1' & 'L8 < L11') -> 'L8 < L1')\",\n",
" \"(('L11 < L1' & 'L9 < L11') -> 'L9 < L1')\",\n",
" \"(('L11 < L10' & 'L13 < L11') -> 'L13 < L10')\",\n",
" \"(('L11 < L10' & 'L8 < L11') -> 'L8 < L10')\",\n",
" \"(('L11 < L12' & 'L1 < L11') -> 'L1 < L12')\",\n",
" \"(('L11 < L12' & 'L10 < L11') -> 'L10 < L12')\",\n",
" \"(('L11 < L12' & 'L12 < L9') -> 'L11 < L9')\",\n",
" \"(('L11 < L12' & 'L13 < L11') -> 'L13 < L12')\",\n",
" \"(('L11 < L12' & 'L14 < L11') -> 'L14 < L12')\",\n",
" \"(('L11 < L12' & 'L15 < L11') -> 'L15 < L12')\",\n",
" \"(('L11 < L12' & 'L16 < L11') -> 'L16 < L12')\",\n",
" \"(('L11 < L12' & 'L17 < L11') -> 'L17 < L12')\",\n",
" \"(('L11 < L12' & 'L18 < L11') -> 'L18 < L12')\",\n",
" \"(('L11 < L12' & 'L19 < L11') -> 'L19 < L12')\",\n",
" \"(('L11 < L12' & 'L3 < L11') -> 'L3 < L12')\",\n",
" \"(('L11 < L12' & 'L4 < L11') -> 'L4 < L12')\",\n",
" \"(('L11 < L12' & 'L5 < L11') -> 'L5 < L12')\",\n",
" \"(('L11 < L12' & 'L6 < L11') -> 'L6 < L12')\",\n",
" \"(('L11 < L12' & 'L7 < L11') -> 'L7 < L12')\",\n",
" \"(('L11 < L12' & 'L8 < L11') -> 'L8 < L12')\",\n",
" \"(('L11 < L13' & 'L10 < L11') -> 'L10 < L13')\",\n",
" \"(('L11 < L13' & 'L13 < L12') -> 'L11 < L12')\",\n",
" \"(('L11 < L13' & 'L13 < L14') -> 'L11 < L14')\",\n",
" \"(('L11 < L13' & 'L13 < L8') -> 'L11 < L8')\",\n",
" \"(('L11 < L13' & 'L7 < L11') -> 'L7 < L13')\",\n",
" \"(('L11 < L13' & 'L8 < L11') -> 'L8 < L13')\",\n",
" \"(('L11 < L13' & 'L9 < L11') -> 'L9 < L13')\",\n",
" \"(('L11 < L14' & 'L10 < L11') -> 'L10 < L14')\",\n",
" \"(('L11 < L14' & 'L12 < L11') -> 'L12 < L14')\",\n",
" \"(('L11 < L14' & 'L13 < L11') -> 'L13 < L14')\",\n",
" \"(('L11 < L14' & 'L14 < L12') -> 'L11 < L12')\",\n",
" \"(('L11 < L14' & 'L14 < L8') -> 'L11 < L8')\",\n",
" \"(('L11 < L14' & 'L14 < L9') -> 'L11 < L9')\",\n",
" \"(('L11 < L14' & 'L15 < L11') -> 'L15 < L14')\",\n",
" \"(('L11 < L14' & 'L18 < L11') -> 'L18 < L14')\",\n",
" \"(('L11 < L14' & 'L3 < L11') -> 'L3 < L14')\",\n",
" \"(('L11 < L14' & 'L5 < L11') -> 'L5 < L14')\",\n",
" \"(('L11 < L14' & 'L7 < L11') -> 'L7 < L14')\",\n",
" \"(('L11 < L14' & 'L8 < L11') -> 'L8 < L14')\",\n",
" \"(('L11 < L14' & 'L9 < L11') -> 'L9 < L14')\",\n",
" \"(('L11 < L15' & 'L7 < L11') -> 'L7 < L15')\",\n",
" \"(('L11 < L15' & 'L8 < L11') -> 'L8 < L15')\",\n",
" \"(('L11 < L16' & 'L16 < L14') -> 'L11 < L14')\",\n",
" \"(('L11 < L16' & 'L16 < L17') -> 'L11 < L17')\",\n",
" \"(('L11 < L16' & 'L16 < L7') -> 'L11 < L7')\",\n",
" \"(('L11 < L16' & 'L8 < L11') -> 'L8 < L16')\",\n",
" \"(('L11 < L16' & 'L9 < L11') -> 'L9 < L16')\",\n",
" \"(('L11 < L17' & 'L0 < L11') -> 'L0 < L17')\",\n",
" \"(('L11 < L17' & 'L10 < L11') -> 'L10 < L17')\",\n",
" \"(('L11 < L17' & 'L12 < L11') -> 'L12 < L17')\",\n",
" \"(('L11 < L17' & 'L17 < L1') -> 'L11 < L1')\",\n",
" \"(('L11 < L17' & 'L17 < L13') -> 'L11 < L13')\",\n",
" \"(('L11 < L17' & 'L17 < L14') -> 'L11 < L14')\",\n",
" \"(('L11 < L17' & 'L17 < L15') -> 'L11 < L15')\",\n",
" \"(('L11 < L17' & 'L17 < L19') -> 'L11 < L19')\",\n",
" \"(('L11 < L17' & 'L17 < L2') -> 'L11 < L2')\",\n",
" \"(('L11 < L17' & 'L17 < L5') -> 'L11 < L5')\",\n",
" \"(('L11 < L17' & 'L17 < L7') -> 'L11 < L7')\",\n",
" \"(('L11 < L17' & 'L17 < L8') -> 'L11 < L8')\",\n",
" \"(('L11 < L17' & 'L18 < L11') -> 'L18 < L17')\",\n",
" \"(('L11 < L17' & 'L3 < L11') -> 'L3 < L17')\",\n",
" \"(('L11 < L17' & 'L6 < L11') -> 'L6 < L17')\",\n",
" \"(('L11 < L17' & 'L7 < L11') -> 'L7 < L17')\",\n",
" \"(('L11 < L17' & 'L8 < L11') -> 'L8 < L17')\",\n",
" \"(('L11 < L17' & 'L9 < L11') -> 'L9 < L17')\",\n",
" \"(('L11 < L18' & 'L13 < L11') -> 'L13 < L18')\",\n",
" \"(('L11 < L18' & 'L18 < L9') -> 'L11 < L9')\",\n",
" \"(('L11 < L18' & 'L19 < L11') -> 'L19 < L18')\",\n",
" \"(('L11 < L18' & 'L7 < L11') -> 'L7 < L18')\",\n",
" \"(('L11 < L18' & 'L8 < L11') -> 'L8 < L18')\",\n",
" \"(('L11 < L19' & 'L0 < L11') -> 'L0 < L19')\",\n",
" \"(('L11 < L19' & 'L15 < L11') -> 'L15 < L19')\",\n",
" \"(('L11 < L19' & 'L18 < L11') -> 'L18 < L19')\",\n",
" \"(('L11 < L19' & 'L19 < L14') -> 'L11 < L14')\",\n",
" \"(('L11 < L19' & 'L19 < L3') -> 'L11 < L3')\",\n",
" \"(('L11 < L19' & 'L6 < L11') -> 'L6 < L19')\",\n",
" \"(('L11 < L19' & 'L8 < L11') -> 'L8 < L19')\",\n",
" \"(('L11 < L19' & 'L9 < L11') -> 'L9 < L19')\",\n",
" \"(('L11 < L2' & 'L2 < L19') -> 'L11 < L19')\",\n",
" \"(('L11 < L2' & 'L2 < L7') -> 'L11 < L7')\",\n",
" \"(('L11 < L2' & 'L8 < L11') -> 'L8 < L2')\",\n",
" \"(('L11 < L2' & 'L9 < L11') -> 'L9 < L2')\",\n",
" \"(('L11 < L3' & 'L13 < L11') -> 'L13 < L3')\",\n",
" \"(('L11 < L3' & 'L8 < L11') -> 'L8 < L3')\",\n",
" \"(('L11 < L3' & 'L9 < L11') -> 'L9 < L3')\",\n",
" \"(('L11 < L4' & 'L4 < L1') -> 'L11 < L1')\",\n",
" \"(('L11 < L4' & 'L4 < L13') -> 'L11 < L13')\",\n",
" \"(('L11 < L4' & 'L4 < L19') -> 'L11 < L19')\",\n",
" \"(('L11 < L4' & 'L4 < L5') -> 'L11 < L5')\",\n",
" \"(('L11 < L4' & 'L4 < L7') -> 'L11 < L7')\",\n",
" \"(('L11 < L4' & 'L8 < L11') -> 'L8 < L4')\",\n",
" \"(('L11 < L4' & 'L9 < L11') -> 'L9 < L4')\",\n",
" \"(('L11 < L5' & 'L13 < L11') -> 'L13 < L5')\",\n",
" \"(('L11 < L5' & 'L15 < L11') -> 'L15 < L5')\",\n",
" \"(('L11 < L5' & 'L18 < L11') -> 'L18 < L5')\",\n",
" \"(('L11 < L5' & 'L6 < L11') -> 'L6 < L5')\",\n",
" \"(('L11 < L5' & 'L8 < L11') -> 'L8 < L5')\",\n",
" \"(('L11 < L5' & 'L9 < L11') -> 'L9 < L5')\",\n",
" \"(('L11 < L6' & 'L7 < L11') -> 'L7 < L6')\",\n",
" \"(('L11 < L8' & 'L1 < L11') -> 'L1 < L8')\",\n",
" \"(('L11 < L8' & 'L10 < L11') -> 'L10 < L8')\",\n",
" \"(('L11 < L8' & 'L12 < L11') -> 'L12 < L8')\",\n",
" \"(('L11 < L8' & 'L13 < L11') -> 'L13 < L8')\",\n",
" \"(('L11 < L8' & 'L14 < L11') -> 'L14 < L8')\",\n",
" \"(('L11 < L8' & 'L15 < L11') -> 'L15 < L8')\",\n",
" \"(('L11 < L8' & 'L16 < L11') -> 'L16 < L8')\",\n",
" \"(('L11 < L8' & 'L17 < L11') -> 'L17 < L8')\",\n",
" \"(('L11 < L8' & 'L18 < L11') -> 'L18 < L8')\",\n",
" \"(('L11 < L8' & 'L19 < L11') -> 'L19 < L8')\",\n",
" \"(('L11 < L8' & 'L2 < L11') -> 'L2 < L8')\",\n",
" \"(('L11 < L8' & 'L3 < L11') -> 'L3 < L8')\",\n",
" \"(('L11 < L8' & 'L4 < L11') -> 'L4 < L8')\",\n",
" \"(('L11 < L8' & 'L5 < L11') -> 'L5 < L8')\",\n",
" \"(('L11 < L8' & 'L7 < L11') -> 'L7 < L8')\",\n",
" \"(('L11 < L8' & 'L8 < L0') -> 'L11 < L0')\",\n",
" \"(('L11 < L8' & 'L8 < L6') -> 'L11 < L6')\",\n",
" \"(('L11 < L8' & 'L8 < L9') -> 'L11 < L9')\",\n",
" \"(('L11 < L9' & 'L13 < L11') -> 'L13 < L9')\",\n",
" \"(('L11 < L9' & 'L2 < L11') -> 'L2 < L9')\",\n",
" \"(('L11 < L9' & 'L7 < L11') -> 'L7 < L9')\",\n",
" \"(('L12 < L1' & 'L1 < L10') -> 'L12 < L10')\",\n",
" \"(('L12 < L1' & 'L1 < L15') -> 'L12 < L15')\",\n",
" \"(('L12 < L1' & 'L1 < L16') -> 'L12 < L16')\",\n",
" \"(('L12 < L1' & 'L1 < L3') -> 'L12 < L3')\",\n",
" \"(('L12 < L1' & 'L1 < L5') -> 'L12 < L5')\",\n",
" \"(('L12 < L1' & 'L1 < L7') -> 'L12 < L7')\",\n",
" \"(('L12 < L1' & 'L15 < L12') -> 'L15 < L1')\",\n",
" \"(('L12 < L1' & 'L18 < L12') -> 'L18 < L1')\",\n",
" \"(('L12 < L1' & 'L6 < L12') -> 'L6 < L1')\",\n",
" \"(('L12 < L1' & 'L8 < L12') -> 'L8 < L1')\",\n",
" \"(('L12 < L1' & 'L9 < L12') -> 'L9 < L1')\",\n",
" \"(('L12 < L10' & 'L10 < L3') -> 'L12 < L3')\",\n",
" \"(('L12 < L10' & 'L18 < L12') -> 'L18 < L10')\",\n",
" \"(('L12 < L11' & 'L11 < L1') -> 'L12 < L1')\",\n",
" \"(('L12 < L11' & 'L11 < L10') -> 'L12 < L10')\",\n",
" \"(('L12 < L11' & 'L11 < L13') -> 'L12 < L13')\",\n",
" \"(('L12 < L11' & 'L11 < L15') -> 'L12 < L15')\",\n",
" \"(('L12 < L11' & 'L11 < L16') -> 'L12 < L16')\",\n",
" \"(('L12 < L11' & 'L11 < L18') -> 'L12 < L18')\",\n",
" \"(('L12 < L11' & 'L11 < L19') -> 'L12 < L19')\",\n",
" \"(('L12 < L11' & 'L11 < L3') -> 'L12 < L3')\",\n",
" \"(('L12 < L11' & 'L11 < L4') -> 'L12 < L4')\",\n",
" \"(('L12 < L11' & 'L11 < L5') -> 'L12 < L5')\",\n",
" \"(('L12 < L11' & 'L11 < L6') -> 'L12 < L6')\",\n",
" \"(('L12 < L11' & 'L11 < L7') -> 'L12 < L7')\",\n",
" \"(('L12 < L13' & 'L13 < L11') -> 'L12 < L11')\",\n",
" \"(('L12 < L13' & 'L13 < L14') -> 'L12 < L14')\",\n",
" \"(('L12 < L13' & 'L13 < L17') -> 'L12 < L17')\",\n",
" \"(('L12 < L13' & 'L13 < L7') -> 'L12 < L7')\",\n",
" \"(('L12 < L13' & 'L13 < L8') -> 'L12 < L8')\",\n",
" \"(('L12 < L14' & 'L14 < L1') -> 'L12 < L1')\",\n",
" \"(('L12 < L14' & 'L14 < L10') -> 'L12 < L10')\",\n",
" \"(('L12 < L14' & 'L14 < L11') -> 'L12 < L11')\",\n",
" \"(('L12 < L14' & 'L14 < L13') -> 'L12 < L13')\",\n",
" \"(('L12 < L14' & 'L14 < L15') -> 'L12 < L15')\",\n",
" \"(('L12 < L14' & 'L14 < L16') -> 'L12 < L16')\",\n",
" \"(('L12 < L14' & 'L14 < L17') -> 'L12 < L17')\",\n",
" \"(('L12 < L14' & 'L14 < L19') -> 'L12 < L19')\",\n",
" \"(('L12 < L14' & 'L14 < L3') -> 'L12 < L3')\",\n",
" \"(('L12 < L14' & 'L14 < L4') -> 'L12 < L4')\",\n",
" \"(('L12 < L14' & 'L14 < L5') -> 'L12 < L5')\",\n",
" \"(('L12 < L14' & 'L14 < L6') -> 'L12 < L6')\",\n",
" \"(('L12 < L14' & 'L14 < L7') -> 'L12 < L7')\",\n",
" \"(('L12 < L14' & 'L14 < L8') -> 'L12 < L8')\",\n",
" ...]"
]
},
"execution_count": 71,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"clauses = sorted(map(str, sat.simplify(VW.sat_cnf(True)).args()))\n",
"# clauses = str(sat.simplify(VW.sat_cnf(True)))[1:-1].split(\" & \")\n",
"# clauses.sort()\n",
"clauses"
]
},
{
"cell_type": "code",
"execution_count": 118,
"id": "b7734f59",
"metadata": {
"pycharm": {
"is_executing": true,
"name": "#%%\n"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"True True False\n",
"2 SAT\n",
"'L5 < L3' := True\n",
"'L5 < [L0, L3]' := True\n",
"'L3 < L5' := False\n",
"'L5 < L0' := True\n",
"'L0 < L5' := False\n",
"\n",
"3 SAT\n",
"'L5 < L3' := True\n",
"'L5 < [L0, L3]' := True\n",
"'L3 < L5' := False\n",
"'L5 < L0' := True\n",
"'L0 < L5' := False\n",
"'L3 < L0' := False\n",
"'L0 < L3' := True\n",
"\n",
"2+3 SAT\n",
"{'L5 < L3', 'L3 < L5', (('L3 < L0' | (! ('L3 < L5' & 'L5 < L0'))) & (('L0 < L3' | (! (... & ...))) & (('L0 < L3' <-> (! ...)) & ((... <-> ...) & (... & ...)))))}\n",
"\n",
"[('U1', 'L1'), ('U1', 'L4'), ('U2', 'L4'), ('U2', 'L5'), ('U3', 'L3'), ('U4', 'L0'), ('U4', 'L3'), ('U6', 'L5')]\n"
]
},
{
"data": {
"text/html": [
"<?xml version=\"1.0\"?>\n",
"<svg xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" xmlns:ev=\"http://www.w3.org/2001/xml-events\" version=\"1.1\" baseProfile=\"full\" viewBox=\"-60.5 -260.5 511 321\">\n",
"\t<g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M0,-200 L400,-200\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M0,0 L400,0\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M100,-200 L100,0\" stroke=\"#AE00C7\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M100,-200 L250,0\" stroke=\"#AE00C7\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M150,-200 L250,0\" stroke=\"#AE00C7\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M150,-200 L300,0\" stroke=\"#AE00C7\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M200,-200 L200,0\" stroke=\"#AE00C7\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M250,-200 L50,0\" stroke=\"#AE00C7\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M250,-200 L200,0\" stroke=\"#AE00C7\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M350,-200 L300,0\" stroke=\"#AE00C7\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"50\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"50\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"100\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"100\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"150\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"150\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"200\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"200\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"250\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"250\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"300\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"300\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">5</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"350\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"350\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">6</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"50\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"50\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"100\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"100\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"150\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"150\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"200\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"200\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"250\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"250\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"300\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"300\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">5</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"350\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"350\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">6</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"-10\" y=\"-210\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"0\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">U</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"400\" y=\"-200\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"400\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"-10\" y=\"-10\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"0\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">L</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"400\" y=\"0\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"400\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n",
"\t</g>\n",
"</svg>\n"
],
"text/plain": [
"<cppyy.gbl.ogdf.GraphAttributes object at 0x556e09326c50>"
]
},
"execution_count": 118,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"for i in range(1000):\n",
" VW = Volkswagen()\n",
" VW.make_graph(7, 7)\n",
" VW.layout()\n",
" density = random.uniform(0.1, 0.3)\n",
" for u in VW.upper:\n",
" for l in VW.lower:\n",
" if random.random() < density:\n",
" VW.new_edge(u,l,ogdf.Color(\"test\"))\n",
" \n",
" sat2 = VW.sat_cnf(trans=False)\n",
" sat3 = VW.sat_cnf(trans=True)\n",
" \n",
" sol = sat.Solver(generate_models=True)\n",
" sol.add_assertion(sat2)\n",
" sat2b = sol.solve()\n",
" sat2m = sol.get_model() if sat2b else None\n",
" \n",
" sol.push()\n",
" sol.add_assertion(sat3)\n",
" sat3b = sol.solve()\n",
" sat3m = sol.get_model() if sat3b else None\n",
" \n",
" sat32b = False\n",
" if sat2b:\n",
" sat32 = [var if val else sat.Not(var) for var,val in sat2m]\n",
" sat32b = sol.solve(sat32)\n",
" if not sat32b:\n",
" print(sat2b, sat3b, sat32b)\n",
" print(\"2 SAT\")\n",
" print(sat2m)\n",
" print(\"\\n3 SAT\")\n",
" print(sat3m)\n",
" print(\"\\n2+3 SAT\")\n",
" print(sat.get_unsat_core([sat3, *sat32]))\n",
" print()\n",
" break\n",
" \n",
" sol.exit()\n",
" \n",
"# sat2b, sat3b = sat.is_sat(sat2), sat.is_sat(sat3)\n",
"# if not sat3b and sat2b:\n",
"# break\n",
"# break\n",
"else:\n",
" print(\"Nothing found\")\n",
"# print(VW.sat_solvable(trans=True))\n",
"# pos = list(VW.try_all(True))\n",
"# sol = VW.sat_solvable()\n",
"# print(bool(pos),sol)\n",
"# print(sat2b,sat3b)\n",
"print(VW.get_edges())\n",
"VW.GA"
]
},
{
"cell_type": "code",
"execution_count": 136,
"id": "65a160c8",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"['L5 < L3',\n",
" 'L3 < L5',\n",
" ('L3 < L0' | (! ('L3 < L5' & 'L5 < L0'))),\n",
" ('L0 < L3' | (! ('L5 < L3' & 'L0 < L5'))),\n",
" ('L0 < L3' <-> (! 'L3 < L0')),\n",
" ('L5 < L3' <-> 'L5 < [L0, L3]'),\n",
" ('L5 < L3' <-> (! 'L3 < L5')),\n",
" ('L5 < L0' <-> 'L5 < [L0, L3]'),\n",
" ('L5 < L0' <-> (! 'L0 < L5'))]\n"
]
}
],
"source": [
"def flatten(clause):\n",
" if isinstance(clause, list):\n",
" for c in clause:\n",
" yield from flatten(c)\n",
" elif clause.is_and():\n",
" for c in clause.args():\n",
" yield from flatten(c)\n",
" else:\n",
" yield clause\n",
"\n",
"unsat = list(flatten(list(sat.get_unsat_core([sat3, *sat32]))))\n",
"from pprint import pprint\n",
"pprint(unsat)"
]
},
{
"cell_type": "code",
"execution_count": 84,
"id": "0ded975b",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"data": {
"text/plain": [
"[('L9 < L5', False),\n",
" ('L9 < [L0, L5]', False),\n",
" ('L9 < L0', False),\n",
" ('L0 < L9', True),\n",
" ('L9 < L6', True),\n",
" ('L9 < [L1, L6]', True),\n",
" ('L6 < L9', False),\n",
" ('L9 < L1', True),\n",
" ('L1 < L9', False),\n",
" ('L7 < L9', True),\n",
" ('L7 < [L0, L2, L9]', True),\n",
" ('L7 < L2', True),\n",
" ('L2 < L7', False),\n",
" ('L7 < L0', True),\n",
" ('L7 < L5', True),\n",
" ('L7 < [L0, L5]', True),\n",
" ('L7 < [L0, L9]', True),\n",
" ('L7 < [L0, L4, L5, L9]', True),\n",
" ('L9 < L7', False),\n",
" ('L5 < L7', False),\n",
" ('L7 < L4', True),\n",
" ('L4 < L7', False),\n",
" ('L0 < L7', False),\n",
" ('L7 < L6', True),\n",
" ('L7 < [L1, L6]', True),\n",
" ('L6 < L7', False),\n",
" ('L7 < L1', True),\n",
" ('L1 < L7', False),\n",
" ('L5 < L9', True),\n",
" ('L5 < [L0, L9]', True),\n",
" ('L5 < L0', True),\n",
" ('L0 < L5', False),\n",
" ('L4 < L6', True),\n",
" ('L4 < [L1, L6]', True),\n",
" ('L6 < L4', False),\n",
" ('L4 < L1', True),\n",
" ('L1 < L4', False),\n",
" ('L3 < L9', True),\n",
" ('L3 < [L0, L4, L5, L9]', True),\n",
" ('L9 < L3', False),\n",
" ('L3 < L5', True),\n",
" ('L5 < L3', False),\n",
" ('L3 < L4', True),\n",
" ('L4 < L3', False),\n",
" ('L3 < L0', True),\n",
" ('L0 < L3', False),\n",
" ('L3 < L6', True),\n",
" ('L3 < [L1, L6]', True),\n",
" ('L6 < L3', False),\n",
" ('L3 < L1', True),\n",
" ('L1 < L3', False)]"
]
},
"execution_count": 84,
"metadata": {},
"output_type": "execute_result"
}
],
"source": []
},
{
"cell_type": "code",
"execution_count": 8,
"id": "2b2d8cf4",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [],
"source": [
"EDGES = [(1,1),(1,2),(2,3),(2,4),(2,7),(3,1),(3,3),(3,6),(4,2),(4,4),(5,6),(5,7)] # (3,5),(4,5)"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "0e384493",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"True True True\n"
]
},
{
"data": {
"text/plain": "<cppyy.gbl.ogdf.GraphAttributes object at 0x562a15428ad0>",
"text/html": "<?xml version=\"1.0\"?>\n<svg xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" xmlns:ev=\"http://www.w3.org/2001/xml-events\" version=\"1.1\" baseProfile=\"full\" viewBox=\"-60.5 -260.5 561 321\">\n\t<g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M0,-200 L450,-200\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M0,0 L450,0\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M100,-200 L50,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M100,-200 L300,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M150,-200 L100,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M150,-200 L250,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M150,-200 L200,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M200,-200 L50,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M200,-200 L100,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M200,-200 L150,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M250,-200 L300,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M250,-200 L250,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M300,-200 L150,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t\t<g>\n\t\t\t<path fill=\"none\" d=\" M300,-200 L200,0\" stroke=\"#0000FF\" stroke-width=\"3.000000px\" />\n\t\t</g>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"50\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"50\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"100\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"100\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"150\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"150\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"200\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"200\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"250\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"250\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"300\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"300\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">5</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"350\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"350\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"50\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"50\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"300\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"300\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"100\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"100\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"250\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"250\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"400\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"400\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">5</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"150\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"150\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">6</text>\n\t</g>\n\t<g>\n\t\t<ellipse cx=\"200\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"200\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">7</text>\n\t</g>\n\t<g>\n\t\t<rect x=\"-10\" y=\"-210\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"0\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">U</text>\n\t</g>\n\t<g>\n\t\t<rect x=\"450\" y=\"-200\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"450\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n\t</g>\n\t<g>\n\t\t<rect x=\"-10\" y=\"-10\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"0\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">L</text>\n\t</g>\n\t<g>\n\t\t<rect x=\"450\" y=\"0\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n\t\t<text x=\"450\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n\t</g>\n</svg>\n"
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"VW = Volkswagen()\n",
"VW.make_graph(6, 8)\n",
"VW.layout()\n",
"for u, l in EDGES:\n",
" VW.new_edge(u,l,ogdf.Color(\"#00F\"))\n",
"pos = list(VW.try_all(True))\n",
"sol = VW.sat_solvable()\n",
"sol3 = VW.sat_solvable(trans=True)\n",
"print(bool(pos), sol, sol3)\n",
"VW.sort(pos[0])\n",
"# while bool(pos) != sol:\n",
"# n = VW.G.chooseNode()\n",
"# if not VW.GA.label[n] or n.degree() == 0 or VW.GA.label[n].decode(\"ascii\") in (\"U\", \"L\"):\n",
"# continue\n",
"# print(n.index(), \"U\" if VW.GA.y[n] < 0 else \"L\", VW.GA.label[n], VW.get_label(n))\n",
"# for e in [adj.theEdge() for adj in n.adjEntries]:\n",
"# VW.G.delEdge(e)\n",
"# pos = list(VW.try_all(True))\n",
"# sol = VW.sat_solvable()\n",
"# print(bool(pos), sol)\n",
"VW.GA"
]
},
{
"cell_type": "code",
"execution_count": 117,
"id": "ff075152",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"L1 : U2 -> U11\n",
" L1 - U5 ['L2', 'L4']\n",
" L1 - U8 ['L3', 'L5']\n",
"L2 : U1 -> U5\n",
" L2 - U2 ['L1', 'L3']\n",
"L3 : U2 -> U8\n",
" L3 - U5 ['L2', 'L4']\n",
"L4 : U5 -> U11\n",
" L4 - U8 ['L3', 'L5']\n",
"L5 : U8 -> U12\n",
" L5 - U11 ['L1', 'L4']\n",
"True True\n"
]
},
{
"data": {
"text/html": [
"<?xml version=\"1.0\"?>\n",
"<svg xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" xmlns:ev=\"http://www.w3.org/2001/xml-events\" version=\"1.1\" baseProfile=\"full\" viewBox=\"-60.5 -260.5 811 321\">\n",
"\t<g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M0,-200 L700,-200\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M0,0 L700,0\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M100,-200 L50,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M150,-200 L150,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M150,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M200,-200 L50,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M250,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M300,-200 L50,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M300,-200 L100,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M350,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M400,-200 L100,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M450,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M450,-200 L250,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M500,-200 L100,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M550,-200 L250,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M600,-200 L150,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M600,-200 L100,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M650,-200 L250,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"50\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"50\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"100\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"100\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"150\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"150\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"200\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"200\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"250\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"250\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"300\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"300\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">5</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"350\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"350\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">6</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"400\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"400\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">7</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"450\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"450\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">8</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"500\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"500\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">9</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"550\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"550\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">10</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"600\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"600\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">11</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"650\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"650\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">12</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"300\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"300\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"150\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"150\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"50\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"50\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"200\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"200\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"100\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"100\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"250\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"250\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">5</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"-10\" y=\"-210\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"0\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">U</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"700\" y=\"-200\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"700\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"-10\" y=\"-10\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"0\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">L</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"700\" y=\"0\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"700\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n",
"\t</g>\n",
"</svg>\n"
],
"text/plain": [
"<cppyy.gbl.ogdf.GraphAttributes object at 0x556e05c1e610>"
]
},
"execution_count": 117,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"VW = Volkswagen()\n",
"VW.make_graph(13, 6)\n",
"VW.layout()\n",
"for u, l in EDGES:\n",
"# if l in [0,2,8] or u in []:\n",
"# continue\n",
" VW.new_edge(u,l,ogdf.Color(\"#0F0\"))\n",
"pos = list(VW.try_all(True))\n",
"sol = VW.sat_solvable()\n",
"list(VW.sat_constraints(True))\n",
"print(bool(pos), sol)\n",
"VW.sort(pos[0])\n",
"VW.GA"
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "152d0fd3",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"L1 : U1 -> U5\n",
" L1 - U4 ['L6', 'L7']\n",
"L3 : U0 -> U6\n",
" L3 - U1 ['L1', 'L7']\n",
" L3 - U4 ['L6', 'L7']\n",
"L4 : U3 -> U6\n",
" L4 - U4 ['L6', 'L7']\n",
" L4 - U5 ['L1', 'L3']\n",
"L6 : U4 -> U8\n",
" L6 - U5 ['L1', 'L3']\n",
" L6 - U6 ['L3', 'L4', 'L7']\n",
"L7 : U1 -> U6\n",
" L7 - U5 ['L1', 'L3']\n",
"True True\n"
]
},
{
"data": {
"text/html": [
"<?xml version=\"1.0\"?>\n",
"<svg xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" xmlns:ev=\"http://www.w3.org/2001/xml-events\" version=\"1.1\" baseProfile=\"full\" viewBox=\"-60.5 -260.5 661 321\">\n",
"\t<g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M0,-200 L550,-200\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M0,0 L550,0\" stroke=\"#CCCCCC\" stroke-width=\"5.000000px\" stroke-dasharray=\"5,10\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M50,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M100,-200 L100,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M100,-200 L400,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M150,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M200,-200 L250,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M250,-200 L350,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M250,-200 L400,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M300,-200 L100,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M300,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M350,-200 L200,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M350,-200 L250,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M350,-200 L400,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t\t<g>\n",
"\t\t\t<path fill=\"none\" d=\" M450,-200 L350,0\" stroke=\"#00FF00\" stroke-width=\"3.000000px\" />\n",
"\t\t</g>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"50\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"50\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"100\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"100\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"150\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"150\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"200\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"200\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"250\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"250\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"300\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"300\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">5</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"350\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"350\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">6</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"400\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"400\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">7</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"450\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"450\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">8</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"500\" cy=\"-200\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"500\" y=\"-210\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">9</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"50\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"50\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">0</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"100\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"100\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">1</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"150\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"150\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">2</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"200\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"200\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">3</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"250\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"250\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">4</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"300\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"300\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">5</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"350\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"350\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">6</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"400\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"400\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">7</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"450\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"450\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">8</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<ellipse cx=\"500\" cy=\"0\" rx=\"5\" ry=\"5\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"500\" y=\"12\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">9</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"-10\" y=\"-210\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"0\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">U</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"550\" y=\"-200\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"550\" y=\"-200\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"-10\" y=\"-10\" width=\"20\" height=\"20\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"0\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\">L</text>\n",
"\t</g>\n",
"\t<g>\n",
"\t\t<rect x=\"550\" y=\"0\" width=\"0\" height=\"0\" fill=\"#FFFFFF\" stroke-width=\"1.000000px\" stroke=\"#000000\" />\n",
"\t\t<text x=\"550\" y=\"0\" text-anchor=\"middle\" dominant-baseline=\"middle\" font-family=\"Arial\" font-size=\"10\" fill=\"#000000\"></text>\n",
"\t</g>\n",
"</svg>\n"
],
"text/plain": [
"<cppyy.gbl.ogdf.GraphAttributes object at 0x556dfc7cd020>"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"VW = Volkswagen()\n",
"VW.make_graph(10, 10)\n",
"VW.layout()\n",
"for u, l in EDGES:\n",
" if l in [0,2,8,5] or u in []:\n",
" continue\n",
" VW.new_edge(u,l,ogdf.Color(\"#0F0\"))\n",
"pos = list(VW.try_all(True))\n",
"sol = VW.sat_solvable()\n",
"list(VW.sat_constraints(True))\n",
"print(bool(pos), sol)\n",
"VW.GA"
]
},
{
"cell_type": "code",
"execution_count": 12,
"id": "c853556f",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"data": {
"text/plain": [
"(('L7 < [L1, L3]' <-> 'L7 < L1') & ('L7 < [L1, L3]' <-> 'L7 < L3') & ('L1 < [L6, L7]' <-> 'L1 < L6') & ('L1 < [L6, L7]' <-> 'L1 < L7') & ('L3 < [L6, L7]' <-> 'L3 < L6') & ('L3 < [L6, L7]' <-> 'L3 < L7') & ('L4 < [L6, L7]' <-> 'L4 < L6') & ('L4 < [L6, L7]' <-> 'L4 < L7') & ('L6 < [L3, L4, L7]' <-> 'L6 < L3') & ('L6 < [L3, L4, L7]' <-> 'L6 < L4') & ('L6 < [L3, L4, L7]' <-> 'L6 < L7') & ('L3 < L1' <-> (! 'L1 < L3')) & ('L1 < L6' <-> (! 'L6 < L1')) & ('L1 < L7' <-> (! 'L7 < L1')) & ('L3 < [L1, L7]' <-> 'L3 < L1') & ('L3 < L7' <-> (! 'L7 < L3')) & ('L3 < [L1, L7]' <-> 'L3 < L7') & ('L3 < L6' <-> (! 'L6 < L3')) & ('L4 < L6' <-> (! 'L6 < L4')) & ('L4 < L7' <-> (! 'L7 < L4')) & ('L4 < L1' <-> (! 'L1 < L4')) & ('L4 < [L1, L3]' <-> 'L4 < L1') & ('L4 < L3' <-> (! 'L3 < L4')) & ('L4 < [L1, L3]' <-> 'L4 < L3') & ('L6 < [L1, L3]' <-> 'L6 < L1') & ('L6 < [L1, L3]' <-> 'L6 < L3') & ('L6 < L7' <-> (! 'L7 < L6')))"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sat.simplify(VW.sat_cnf())"
]
},
{
"cell_type": "code",
"execution_count": 13,
"id": "0f8d1bc4",
"metadata": {
"pycharm": {
"name": "#%%\n"
}
},
"outputs": [
{
"data": {
"text/plain": [
"defaultdict(list,\n",
" {b'1': [b'6', b'7'],\n",
" b'3': [b'1', b'7', b'6', b'7'],\n",
" b'4': [b'6', b'7', b'1', b'3'],\n",
" b'6': [b'1', b'3', b'3', b'4', b'7'],\n",
" b'7': [b'1', b'3']})"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"VW.sat_dict()"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "homonolo",
"language": "python",
"name": "homonolo"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.11.0"
}
},
"nbformat": 4,
"nbformat_minor": 5
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment