add DPLL notebook

362861de · Michael Leuschel · 8af11212 · 362861de
Commit 362861de authored Nov 11, 2022 by Michael Leuschel
--- a/logic_programming/4_DPLL.ipynb
+++ b/logic_programming/4_DPLL.ipynb
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "9eb5530a",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "source": [
+    "We can convert our Knights and Knaves puzzle to conjunctive normal form\n",
+    "\n",
+    "```\n",
+    "(A ⇔ B  C)  ∧ (B ⇔ A)\n",
+    "(A → B  C)  ∧ (B  C → A)  ∧ (B → A)∧ (A → B)\n",
+    "(A  B  C)  ∧ ((B  C)  A)  ∧ (B  A)∧ (A  B)\n",
+    "(A  B  C)  ∧ ((B ∧ C)  A)  ∧ (B  A)∧ (A  B)\n",
+    "(A  B  C)  ∧ (B  A)  ∧ (C  A)  ∧(B  A)∧ (A  B)\n",
+    "{A  B  C,  B  A,  C  A,  B  A,  A  B}\n",
+    "```\n",
+    "\n",
+    "Below is an encoding of the cnf as a list of lists."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "id": "964ebd52",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    ":- discontiguous problem/3.\n",
+    ":- dynamic problem/3.\n",
+    "problem(1,'Knights & Knaves',\n",
+    "   [ [neg(a),neg(b),neg(c)],\n",
+    "     [pos(b),pos(a)],\n",
+    "     [pos(c),pos(a)],\n",
+    "     [neg(b),pos(a)],\n",
+    "     [neg(a),pos(b)] ]).\n",
+    "negate(pos(A),neg(A)).\n",
+    "negate(neg(A),pos(A))."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "fc6823ad",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "source": [
+    "We can pick two clauses and resolve them as follows:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "id": "152289b6",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mClauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+       "C1 = [neg(a),neg(b),neg(c)],\n",
+       "Lit1 = neg(a)"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- problem(1,_,Clauses),\n",
+    "   member(C1,Clauses), member(Lit1,C1)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "id": "2c3dd1bf",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mClauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+       "C1 = [neg(a),neg(b),neg(c)],\n",
+       "Lit1 = neg(a),\n",
+       "Lit2 = pos(a),\n",
+       "C2 = [pos(b),pos(a)]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- problem(1,_,Clauses),\n",
+    "   member(C1,Clauses), member(Lit1,C1), negate(Lit1,Lit2),\n",
+    "   member(C2,Clauses), member(Lit2,C2).\n",
+    "%comment."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "id": "33fc6271",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    ":- use_module(library(lists)).\n",
+    "resolve(Clause1,Clause2,Resolvent) :- \n",
+    "   select(Lit1,Clause1,R1), negate(Lit1,NLit1),\n",
+    "   select(NLit1,Clause2,R2),\n",
+    "   append(R1,R2,Resolvent)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "id": "78163b60",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mClauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+       "C1 = [neg(a),neg(b),neg(c)],\n",
+       "C2 = [pos(b),pos(a)],\n",
+       "NewClause = [neg(b),neg(c),pos(b)]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- problem(1,_,Clauses),\n",
+    "   member(C1,Clauses), member(C2,Clauses), \n",
+    "   resolve(C1,C2,NewClause)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 15,
+   "id": "9d3fbd1a",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mClauses = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+       "NewClauses = [[neg(b),neg(c),pos(b)],[neg(a),neg(c),pos(a)],[neg(b),neg(c),pos(c)],[neg(a),neg(b),pos(a)],[neg(b),neg(c),neg(b)],[neg(a),neg(c),neg(a)],[pos(a),neg(a),neg(c)],[pos(b),neg(b),neg(c)],[pos(a),pos(a)],[pos(b),pos(b)],[pos(a),neg(a),neg(b)],[pos(c),neg(b),neg(c)],[pos(c),pos(b)],[neg(b),neg(b),neg(c)],[pos(a),pos(a)],[pos(a),neg(a)],[neg(b),pos(b)],[neg(a),neg(a),neg(c)],[pos(b),pos(b)],[pos(b),pos(c)],[pos(b),neg(b)],[neg(a),pos(a)]]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- problem(1,_,Clauses),\n",
+    "   findall(NewClause,(member(C1,Clauses), member(C2,Clauses), \n",
+    "                      resolve(C1,C2,NewClause)), NewClauses)."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "d32921c9",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "source": [
+    "### DPLL Algorithm\n",
+    "\n",
+    "We now present bit by bit the DPLL algorithm as a Prolog program\n",
+    "manipulating the above clause database."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "id": "26924712",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "becomes_true(TrueLit,Clause) :-\n",
+    "    member(TrueLit,Clause).  "
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "17dd1525",
+   "metadata": {},
+   "source": [
+    "The above checks if making a given literal true makes the second argument, a clause, true:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "id": "7d90c4ad",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- becomes_true(pos(b),[neg(a),pos(b)])."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 18,
+   "id": "d4b4e71f",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- becomes_true(neg(a),[neg(a),pos(b)])."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 19,
+   "id": "3b9c87e4",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "simplify(TrueLit,Clause,SimplifedClause) :-\n",
+    "   negate(TrueLit,FalseLit),\n",
+    "   delete(Clause,FalseLit,SimplifedClause).   % Resolution with TrueLit\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 20,
+   "id": "0abd90f6",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mR = [neg(b),neg(c)]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- simplify(pos(a),[neg(a),neg(b),neg(c)],R)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 21,
+   "id": "cc81b404",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mR = [b,c]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- delete([a,b,c],a,R)."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "53d21e85",
+   "metadata": {},
+   "source": [
+    "The above code simplifies a clause by resolution:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 22,
+   "id": "57df05f0",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mSC = [pos(a)]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- simplify(pos(c),[pos(a),neg(c)],SC)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 23,
+   "id": "a36a54a4",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mSC = [pos(a),neg(c)]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- simplify(pos(b),[pos(a),neg(c)],SC)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 24,
+   "id": "95fcf64b",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "set_literal(Lit,Clauses,NewClauses) :-\n",
+    "   exclude(becomes_true(Lit),Clauses,Clauses2),\n",
+    "   maplist(simplify(Lit),Clauses2,NewClauses).\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "f0a8731d",
+   "metadata": {},
+   "source": [
+    "The above code sets a given literal ```Lit``` to true by removing\n",
+    "all now redundant clauses and simplifying the remaining ones via resolution."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 25,
+   "id": "9c35b0b3",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mR = [[neg(b)]]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- exclude(becomes_true(pos(a)), [[neg(b)], [pos(a),pos(c)]],R)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 26,
+   "id": "8259d2d7",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mR = [[neg(b)],[pos(a)]]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- maplist(simplify(neg(c)), [[neg(b),pos(c)], [pos(a),pos(c)]],R)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 27,
+   "id": "25b19d82",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mRes = [[neg(b),neg(c)]]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- set_literal(pos(a),[[neg(a),neg(b),neg(c)]],Res)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 28,
+   "id": "5535384f",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mT = Knights & Knaves,\n",
+       "C1 = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+       "C2 = [[neg(b),neg(c)],[pos(b)]]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- problem(1,T,C1), set_literal(pos(a),C1,C2).\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 29,
+   "id": "592fcdd9",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mC1 = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+       "C2 = [[neg(b),neg(c)],[pos(b)]],\n",
+       "C3 = [[neg(c)]]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- problem(1,_,C1), set_literal(pos(a),C1,C2), set_literal(pos(b),C2,C3)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 30,
+   "id": "b8cabba2",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "dpll(Clauses,[unit(Lit)|Stack]) :-\n",
+    "    select([Lit],Clauses,Clauses2), % unit clause found\n",
+    "    set_literal(Lit,Clauses2,Clauses3),\n",
+    "    dpll(Clauses3,Stack).\n",
+    "dpll([],Stack) :- !, Stack=[]. % SAT\n",
+    "dpll(Clauses,[branch(Lit)|Stack]) :-\n",
+    "    \\+ member([],Clauses), % no inconsistency\n",
+    "    choose_literal(Clauses,Lit),\n",
+    "    set_literal(Lit,Clauses,Clauses2),\n",
+    "    dpll(Clauses2,Stack).    \n",
+    "\n",
+    "choose_literal([ [Lit|_] | _], Lit).\n",
+    "choose_literal([ [Lit|_] | _], NegLit) :-\n",
+    "      negate(Lit,NegLit).\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 31,
+   "id": "e369355c",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mC1 = [[neg(a),neg(b),neg(c)],[pos(b),pos(a)],[pos(c),pos(a)],[neg(b),pos(a)],[neg(a),pos(b)]],\n",
+       "Stack = [branch(pos(a)),unit(pos(b)),unit(neg(c))]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- problem(1,_,C1), dpll(C1,Stack).\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 32,
+   "id": "78764141",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "\n",
+    "test(Nr) :- problem(Nr,Str,Clauses),\n",
+    "            format('Solving problem ~w : ~w~n',[Nr,Str]),\n",
+    "            (dpll(Clauses,Stack)\n",
+    "              -> format('SAT: Model found: ~w~n',[Stack])\n",
+    "              ; format('UNSAT: no model exists',[]))."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 33,
+   "id": "c51455cf",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Solving problem 1 : Knights & Knaves\n",
+       "SAT: Model found: [branch(pos(a)),unit(pos(b)),unit(neg(c))]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- test(1)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 34,
+   "id": "b0466a5d",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "\n",
+    "\n",
+    "problem(2,'Knights & Knaves (Proof by contradiction)',\n",
+    "   [ [neg(a),neg(b),neg(c)],\n",
+    "     [pos(b),pos(a)],\n",
+    "     [pos(c),pos(a)],\n",
+    "     [neg(b),pos(a)],\n",
+    "     [neg(a),pos(b)],\n",
+    "     [neg(a),neg(b),pos(c)] ]).  % <--- negated Query\n",
+    "problem(3,'Princess & Tiger',\n",
+    "     [[pos(t1),pos(z2),neg(t1)],\n",
+    "      [pos(t1),neg(z2)],\n",
+    "      [neg(t1),neg(z2)],\n",
+    "      [pos(t1),pos(z1),neg(t2)],\n",
+    "      [pos(t2),neg(z1)],\n",
+    "      [neg(t1),neg(z1)],\n",
+    "      [pos(z1),pos(z2)],\n",
+    "      [neg(z1),neg(z2)]])."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 36,
+   "id": "2df16148",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Solving problem 2 : Knights & Knaves (Proof by contradiction)\n",
+       "UNSAT: no model exists"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- test(2)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 37,
+   "id": "8d8cf76a",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Solving problem 3 : Princess & Tiger\n",
+       "SAT: Model found: [branch(neg(t1)),unit(neg(z2)),unit(pos(z1)),unit(pos(t2))]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- test(3)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 35,
+   "id": "31d1b945",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "problem(4,'uf-20-02',\n",
+    "  [[ neg(x10) , neg(x16) , pos(x5) ] ,\n",
+    "   [ pos(x16) , neg(x6) , pos(x5) ] ,\n",
+    "   [ neg(x17) , neg(x14) , neg(x18) ] ,\n",
+    "   [ neg(x10) , neg(x15) , pos(x19) ] ,\n",
+    "   [ neg(x1) , neg(x9) , neg(x18) ] ,\n",
+    "   [ pos(x3) , pos(x7) , neg(x6) ] ,\n",
+    "   [ neg(x13) , pos(x1) , pos(x6) ] ,\n",
+    "   [ neg(x2) , neg(x16) , neg(x20) ] ,\n",
+    "   [ pos(x7) , pos(x8) , pos(x18) ] ,\n",
+    "   [ neg(x7) , pos(x10) , neg(x20) ] ,\n",
+    "   [ pos(x2) , neg(x14) , neg(x17) ] ,\n",
+    "   [ pos(x2) , pos(x1) , pos(x19) ] ,\n",
+    "   [ pos(x7) , neg(x20) , neg(x1) ] ,\n",
+    "   [ neg(x11) , pos(x1) , neg(x17) ] ,\n",
+    "   [ pos(x3) , neg(x12) , pos(x19) ] ,\n",
+    "   [ neg(x3) , neg(x13) , pos(x6) ] ,\n",
+    "   [ neg(x13) , pos(x3) , neg(x12) ] ,\n",
+    "   [ pos(x5) , neg(x7) , neg(x12) ] ,\n",
+    "   [ pos(x20) , pos(x8) , neg(x16) ] ,\n",
+    "   [ neg(x13) , neg(x6) , pos(x19) ] ,\n",
+    "   [ neg(x5) , pos(x1) , pos(x14) ] ,\n",
+    "   [ pos(x9) , neg(x5) , pos(x18) ] ,\n",
+    "   [ neg(x12) , neg(x17) , neg(x1) ] ,\n",
+    "   [ neg(x20) , neg(x16) , pos(x19) ] ,\n",
+    "   [ pos(x12) , pos(x10) , neg(x11) ] ,\n",
+    "   [ pos(x6) , neg(x7) , neg(x2) ] ,\n",
+    "   [ pos(x13) , neg(x10) , pos(x17) ] ,\n",
+    "   [ neg(x20) , pos(x8) , neg(x16) ] ,\n",
+    "   [ neg(x10) , neg(x1) , neg(x8) ] ,\n",
+    "   [ neg(x7) , neg(x3) , pos(x19) ] ,\n",
+    "   [ pos(x19) , neg(x1) , neg(x6) ] ,\n",
+    "   [ pos(x19) , neg(x2) , pos(x13) ] ,\n",
+    "   [ neg(x2) , pos(x20) , neg(x9) ] ,\n",
+    "   [ neg(x8) , neg(x20) , pos(x16) ] ,\n",
+    "   [ neg(x13) , neg(x1) , pos(x11) ] ,\n",
+    "   [ pos(x15) , neg(x12) , neg(x6) ] ,\n",
+    "   [ neg(x17) , neg(x19) , pos(x9) ] ,\n",
+    "   [ pos(x19) , neg(x18) , pos(x16) ] ,\n",
+    "   [ pos(x7) , neg(x8) , neg(x19) ] ,\n",
+    "   [ neg(x3) , neg(x7) , neg(x1) ] ,\n",
+    "   [ pos(x7) , neg(x17) , neg(x16) ] ,\n",
+    "   [ neg(x2) , neg(x14) , pos(x1) ] ,\n",
+    "   [ neg(x18) , neg(x10) , neg(x8) ] ,\n",
+    "   [ neg(x16) , pos(x5) , pos(x8) ] ,\n",
+    "   [ pos(x4) , pos(x8) , pos(x10) ] ,\n",
+    "   [ neg(x20) , neg(x11) , neg(x19) ] ,\n",
+    "   [ pos(x8) , neg(x16) , neg(x6) ] ,\n",
+    "   [ pos(x18) , pos(x12) , pos(x8) ] ,\n",
+    "   [ neg(x5) , neg(x20) , neg(x10) ] ,\n",
+    "   [ pos(x16) , pos(x17) , pos(x3) ] ,\n",
+    "   [ pos(x7) , neg(x1) , neg(x17) ] ,\n",
+    "   [ pos(x17) , neg(x4) , pos(x7) ] ,\n",
+    "   [ pos(x20) , neg(x9) , neg(x13) ] ,\n",
+    "   [ pos(x13) , pos(x18) , pos(x16) ] ,\n",
+    "   [ neg(x16) , neg(x6) , pos(x5) ] ,\n",
+    "   [ pos(x5) , pos(x17) , pos(x7) ] ,\n",
+    "   [ neg(x12) , neg(x17) , neg(x6) ] ,\n",
+    "   [ neg(x20) , pos(x19) , neg(x5) ] ,\n",
+    "   [ pos(x9) , neg(x19) , pos(x16) ] ,\n",
+    "   [ neg(x13) , neg(x16) , pos(x11) ] ,\n",
+    "   [ neg(x4) , neg(x19) , neg(x18) ] ,\n",
+    "   [ neg(x13) , pos(x10) , neg(x15) ] ,\n",
+    "   [ pos(x16) , neg(x7) , neg(x14) ] ,\n",
+    "   [ neg(x19) , neg(x7) , neg(x18) ] ,\n",
+    "   [ neg(x20) , pos(x5) , pos(x13) ] ,\n",
+    "   [ pos(x12) , neg(x6) , pos(x4) ] ,\n",
+    "   [ pos(x7) , pos(x9) , neg(x13) ] ,\n",
+    "   [ pos(x16) , pos(x3) , pos(x7) ] ,\n",
+    "   [ pos(x9) , neg(x1) , pos(x12) ] ,\n",
+    "   [ neg(x3) , pos(x14) , pos(x7) ] ,\n",
+    "   [ pos(x1) , pos(x15) , pos(x14) ] ,\n",
+    "   [ neg(x8) , neg(x11) , pos(x18) ] ,\n",
+    "   [ pos(x19) , neg(x9) , pos(x7) ] ,\n",
+    "   [ neg(x10) , pos(x6) , pos(x2) ] ,\n",
+    "   [ pos(x14) , pos(x18) , neg(x11) ] ,\n",
+    "   [ neg(x9) , neg(x16) , pos(x14) ] ,\n",
+    "   [ pos(x1) , pos(x11) , neg(x20) ] ,\n",
+    "   [ pos(x11) , pos(x12) , neg(x4) ] ,\n",
+    "   [ pos(x13) , neg(x11) , neg(x14) ] ,\n",
+    "   [ pos(x17) , neg(x12) , pos(x9) ] ,\n",
+    "   [ pos(x14) , pos(x9) , pos(x1) ] ,\n",
+    "   [ pos(x8) , pos(x19) , pos(x4) ] ,\n",
+    "   [ pos(x6) , neg(x13) , neg(x20) ] ,\n",
+    "   [ neg(x2) , neg(x13) , pos(x11) ] ,\n",
+    "   [ pos(x14) , neg(x13) , pos(x17) ] ,\n",
+    "   [ pos(x9) , neg(x11) , pos(x18) ] ,\n",
+    "   [ neg(x13) , neg(x6) , pos(x5) ] ,\n",
+    "   [ pos(x5) , pos(x19) , neg(x18) ] ,\n",
+    "   [ neg(x4) , pos(x10) , pos(x11) ] ,\n",
+    "   [ neg(x18) , neg(x19) , neg(x20) ] ,\n",
+    "   [ pos(x3) , neg(x9) , pos(x8) ] \n",
+    "   ]).\n",
+    "problem(5,'schaltung_a1.pl',\n",
+    "  [\n",
+    "%a. not_b. c. not_d. e.\n",
+    "    [pos(a)], [neg(b)], [pos(c)], [neg(d)], [pos(e)],\n",
+    "% Schaltungen der ersten Ebene\n",
+    "%and11 :- a,b.\n",
+    "     [pos(and11),neg(a),neg(b)],   \n",
+    "%or11 :- b.\n",
+    "     [pos(or11),neg(b)],\n",
+    "%or11 :- c.\n",
+    "     [pos(or11),neg(b)],\n",
+    "%and12 :- c,d.\n",
+    "     [pos(and12),neg(c),neg(d)],   \n",
+    "%not1 :- not_e.\n",
+    "     [pos(not1),pos(e)],\n",
+    "% Schaltungen der zweiten Ebene\n",
+    "%or21 :- and11.\n",
+    "     [pos(or21),neg(and11)],\n",
+    "%or21 :- not1.\n",
+    "     [pos(or21),neg(not1)],\n",
+    "%and2 :- or11, not1.\n",
+    "     [pos(and2),neg(or11),neg(not1)], \n",
+    "%or22 :- and12.\n",
+    "     [pos(or22),neg(and12)],\n",
+    "%or22 :- not1.\n",
+    "     [pos(or22),neg(not1)],\n",
+    "%not2 :- e.  % \\+ not1.\n",
+    "     [pos(not2),neg(e)],\n",
+    "% Schaltungen der dritten Ebene\n",
+    "%and3 :- or21, and2.\n",
+    "     [pos(and3),neg(or21),neg(and2)], \n",
+    "%or3 :- or22.\n",
+    "     [pos(or3),neg(or22)],\n",
+    "%or3 :- not2.\n",
+    "     [pos(or3),neg(not2)],\n",
+    "% Schaltungen der vierten Ebene\n",
+    "%or4 :- and3.\n",
+    "     [pos(or4),neg(and3)],\n",
+    "%or4 :- or3.\n",
+    "     [pos(or4),neg(or3)],\n",
+    "%and4 :- or3, not2.\n",
+    "     [pos(and4),neg(or3),neg(not2)], \n",
+    "% Letzte Ebene\n",
+    "%and5 :- and4, or4.\n",
+    "     [pos(and5),neg(and4),neg(or4)], \n",
+    "%output :- and5.\n",
+    "     [pos(output),neg(and5)],\n",
+    "% ?- output.\n",
+    "     [neg(output)]\n",
+    "   ]).\n",
+    "\n",
+    "problem(6, 'doodle-wo-max1-constraint',\n",
+    " [ \n",
+    "   [pos(x1),pos(x3)],\n",
+    "   [neg(x3)],\n",
+    "   [neg(x5)],\n",
+    "   [pos(x4),pos(x5)]\n",
+    "  ]).\n",
+    "problem(7, 'doodle-with-max1-constraint',\n",
+    " [ \n",
+    "   [pos(x1),pos(x3)],\n",
+    "   [neg(x3)],\n",
+    "   [neg(x5)],\n",
+    "   [pos(x4),pos(x5)],\n",
+    "   \n",
+    "   [neg(x1),neg(x2)], [neg(x1),neg(x3)], [neg(x1),neg(x4)],\n",
+    "   [neg(x1),neg(x5)],\n",
+    "   [neg(x2),neg(x3)], [neg(x2),neg(x4)],[neg(x2),neg(x5)],\n",
+    "   [neg(x3),neg(x4)],[neg(x3),neg(x5)],\n",
+    "   [neg(x4),neg(x5)]\n",
+    "  ])."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 38,
+   "id": "c51f1ce6",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Solving problem 4 : uf-20-02\n",
+       "SAT: Model found: [branch(neg(x10)),branch(pos(x16)),branch(neg(x17)),branch(neg(x1)),branch(pos(x3)),branch(neg(x13)),branch(neg(x2)),unit(pos(x19)),branch(pos(x7)),unit(neg(x20)),unit(pos(x8)),unit(neg(x18)),unit(neg(x11)),unit(neg(x4)),branch(pos(x5)),unit(pos(x14)),unit(pos(x9)),branch(pos(x15)),branch(pos(x12))]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- test(4)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "bc767ce8",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Prolog",
+   "language": "prolog",
+   "name": "prolog_kernel"
+  },
+  "language_info": {
+   "codemirror_mode": "prolog",
+   "file_extension": ".pl",
+   "mimetype": "text/x-prolog",
+   "name": "Prolog"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
+%% Cell type:markdown id:9eb5530a tags:
+
+We can convert our Knights and Knaves puzzle to conjunctive normal form
+
+```
+(A ⇔ B  C)  ∧ (B ⇔ A)
+(A → B  C)  ∧ (B  C → A)  ∧ (B → A)∧ (A → B)
+(A  B  C)  ∧ ((B  C)  A)  ∧ (B  A)∧ (A  B)
+(A  B  C)  ∧ ((B ∧ C)  A)  ∧ (B  A)∧ (A  B)
+(A  B  C)  ∧ (B  A)  ∧ (C  A)  ∧(B  A)∧ (A  B)
+{A  B  C,  B  A,  C  A,  B  A,  A  B}
+```
+
+Below is an encoding of the cnf as a list of lists.
+
+%% Cell type:code id:964ebd52 tags:
+
+``` prolog
+:- discontiguous problem/3.
+:- dynamic problem/3.
+problem(1,'Knights & Knaves',
+   [ [neg(a),neg(b),neg(c)],
+     [pos(b),pos(a)],
+     [pos(c),pos(a)],
+     [neg(b),pos(a)],
+     [neg(a),pos(b)] ]).
+negate(pos(A),neg(A)).
+negate(neg(A),pos(A)).
+```
+
+%% Cell type:markdown id:fc6823ad tags:
+
+We can pick two clauses and resolve them as follows:
+
+%% Cell type:code id:152289b6 tags:
+
+``` prolog
+?- problem(1,_,Clauses),
+   member(C1,Clauses), member(Lit1,C1).
+```
+
+%% Output
+
+
+%% Cell type:code id:2c3dd1bf tags:
+
+``` prolog
+?- problem(1,_,Clauses),
+   member(C1,Clauses), member(Lit1,C1), negate(Lit1,Lit2),
+   member(C2,Clauses), member(Lit2,C2).
+%comment.
+```
+
+%% Output
+
+
+%% Cell type:code id:33fc6271 tags:
+
+``` prolog
+:- use_module(library(lists)).
+resolve(Clause1,Clause2,Resolvent) :-
+   select(Lit1,Clause1,R1), negate(Lit1,NLit1),
+   select(NLit1,Clause2,R2),
+   append(R1,R2,Resolvent).
+```
+
+%% Cell type:code id:78163b60 tags:
+
+``` prolog
+?- problem(1,_,Clauses),
+   member(C1,Clauses), member(C2,Clauses),
+   resolve(C1,C2,NewClause).
+```
+
+%% Output
+
+
+%% Cell type:code id:9d3fbd1a tags:
+
+``` prolog
+?- problem(1,_,Clauses),
+   findall(NewClause,(member(C1,Clauses), member(C2,Clauses),
+                      resolve(C1,C2,NewClause)), NewClauses).
+```
+
+%% Output
+
+
+%% Cell type:markdown id:d32921c9 tags:
+
+### DPLL Algorithm
+
+We now present bit by bit the DPLL algorithm as a Prolog program
+manipulating the above clause database.
+
+%% Cell type:code id:26924712 tags:
+
+``` prolog
+becomes_true(TrueLit,Clause) :-
+    member(TrueLit,Clause).
+```
+
+%% Cell type:markdown id:17dd1525 tags:
+
+The above checks if making a given literal true makes the second argument, a clause, true:
+
+%% Cell type:code id:7d90c4ad tags:
+
+``` prolog
+?- becomes_true(pos(b),[neg(a),pos(b)]).
+```
+
+%% Output
+
+
+%% Cell type:code id:d4b4e71f tags:
+
+``` prolog
+?- becomes_true(neg(a),[neg(a),pos(b)]).
+```
+
+%% Output
+
+
+%% Cell type:code id:3b9c87e4 tags:
+
+``` prolog
+simplify(TrueLit,Clause,SimplifedClause) :-
+   negate(TrueLit,FalseLit),
+   delete(Clause,FalseLit,SimplifedClause).   % Resolution with TrueLit
+```
+
+%% Cell type:code id:0abd90f6 tags:
+
+``` prolog
+?- simplify(pos(a),[neg(a),neg(b),neg(c)],R).
+```
+
+%% Output
+
+
+%% Cell type:code id:cc81b404 tags:
+
+``` prolog
+?- delete([a,b,c],a,R).
+```
+
+%% Output
+
+
+%% Cell type:markdown id:53d21e85 tags:
+
+The above code simplifies a clause by resolution:
+
+%% Cell type:code id:57df05f0 tags:
+
+``` prolog
+?- simplify(pos(c),[pos(a),neg(c)],SC).
+```
+
+%% Output
+
+
+%% Cell type:code id:a36a54a4 tags:
+
+``` prolog
+?- simplify(pos(b),[pos(a),neg(c)],SC).
+```
+
+%% Output
+
+
+%% Cell type:code id:95fcf64b tags:
+
+``` prolog
+set_literal(Lit,Clauses,NewClauses) :-
+   exclude(becomes_true(Lit),Clauses,Clauses2),
+   maplist(simplify(Lit),Clauses2,NewClauses).
+```
+
+%% Cell type:markdown id:f0a8731d tags:
+
+The above code sets a given literal ```Lit``` to true by removing
+all now redundant clauses and simplifying the remaining ones via resolution.
+
+%% Cell type:code id:9c35b0b3 tags:
+
+``` prolog
+?- exclude(becomes_true(pos(a)), [[neg(b)], [pos(a),pos(c)]],R).
+```
+
+%% Output
+
+
+%% Cell type:code id:8259d2d7 tags:
+
+``` prolog
+?- maplist(simplify(neg(c)), [[neg(b),pos(c)], [pos(a),pos(c)]],R).
+```
+
+%% Output
+
+
+%% Cell type:code id:25b19d82 tags:
+
+``` prolog
+?- set_literal(pos(a),[[neg(a),neg(b),neg(c)]],Res).
+```
+
+%% Output
+
+
+%% Cell type:code id:5535384f tags:
+
+``` prolog
+?- problem(1,T,C1), set_literal(pos(a),C1,C2).
+```
+
+%% Output
+
+
+%% Cell type:code id:592fcdd9 tags:
+
+``` prolog
+?- problem(1,_,C1), set_literal(pos(a),C1,C2), set_literal(pos(b),C2,C3).
+```
+
+%% Output
+
+
+%% Cell type:code id:b8cabba2 tags:
+
+``` prolog
+dpll(Clauses,[unit(Lit)|Stack]) :-
+    select([Lit],Clauses,Clauses2), % unit clause found
+    set_literal(Lit,Clauses2,Clauses3),
+    dpll(Clauses3,Stack).
+dpll([],Stack) :- !, Stack=[]. % SAT
+dpll(Clauses,[branch(Lit)|Stack]) :-
+    \+ member([],Clauses), % no inconsistency
+    choose_literal(Clauses,Lit),
+    set_literal(Lit,Clauses,Clauses2),
+    dpll(Clauses2,Stack).
+
+choose_literal([ [Lit|_] | _], Lit).
+choose_literal([ [Lit|_] | _], NegLit) :-
+      negate(Lit,NegLit).
+```
+
+%% Cell type:code id:e369355c tags:
+
+``` prolog
+?- problem(1,_,C1), dpll(C1,Stack).
+```
+
+%% Output
+
+
+%% Cell type:code id:78764141 tags:
+
+``` prolog
+
+test(Nr) :- problem(Nr,Str,Clauses),
+            format('Solving problem ~w : ~w~n',[Nr,Str]),
+            (dpll(Clauses,Stack)
+              -> format('SAT: Model found: ~w~n',[Stack])
+              ; format('UNSAT: no model exists',[])).
+```
+
+%% Cell type:code id:c51455cf tags:
+
+``` prolog
+?- test(1).
+```
+
+%% Output
+
+
+
+%% Cell type:code id:b0466a5d tags:
+
+``` prolog
+
+
+problem(2,'Knights & Knaves (Proof by contradiction)',
+   [ [neg(a),neg(b),neg(c)],
+     [pos(b),pos(a)],
+     [pos(c),pos(a)],
+     [neg(b),pos(a)],
+     [neg(a),pos(b)],
+     [neg(a),neg(b),pos(c)] ]).  % <--- negated Query
+problem(3,'Princess & Tiger',
+     [[pos(t1),pos(z2),neg(t1)],
+      [pos(t1),neg(z2)],
+      [neg(t1),neg(z2)],
+      [pos(t1),pos(z1),neg(t2)],
+      [pos(t2),neg(z1)],
+      [neg(t1),neg(z1)],
+      [pos(z1),pos(z2)],
+      [neg(z1),neg(z2)]]).
+```
+
+%% Cell type:code id:2df16148 tags:
+
+``` prolog
+?- test(2).
+```
+
+%% Output
+
+
+
+%% Cell type:code id:8d8cf76a tags:
+
+``` prolog
+?- test(3).
+```
+
+%% Output
+
+
+
+%% Cell type:code id:31d1b945 tags:
+
+``` prolog
+problem(4,'uf-20-02',
+  [[ neg(x10) , neg(x16) , pos(x5) ] ,
+   [ pos(x16) , neg(x6) , pos(x5) ] ,
+   [ neg(x17) , neg(x14) , neg(x18) ] ,
+   [ neg(x10) , neg(x15) , pos(x19) ] ,
+   [ neg(x1) , neg(x9) , neg(x18) ] ,
+   [ pos(x3) , pos(x7) , neg(x6) ] ,
+   [ neg(x13) , pos(x1) , pos(x6) ] ,
+   [ neg(x2) , neg(x16) , neg(x20) ] ,
+   [ pos(x7) , pos(x8) , pos(x18) ] ,
+   [ neg(x7) , pos(x10) , neg(x20) ] ,
+   [ pos(x2) , neg(x14) , neg(x17) ] ,
+   [ pos(x2) , pos(x1) , pos(x19) ] ,
+   [ pos(x7) , neg(x20) , neg(x1) ] ,
+   [ neg(x11) , pos(x1) , neg(x17) ] ,
+   [ pos(x3) , neg(x12) , pos(x19) ] ,
+   [ neg(x3) , neg(x13) , pos(x6) ] ,
+   [ neg(x13) , pos(x3) , neg(x12) ] ,
+   [ pos(x5) , neg(x7) , neg(x12) ] ,
+   [ pos(x20) , pos(x8) , neg(x16) ] ,
+   [ neg(x13) , neg(x6) , pos(x19) ] ,
+   [ neg(x5) , pos(x1) , pos(x14) ] ,
+   [ pos(x9) , neg(x5) , pos(x18) ] ,
+   [ neg(x12) , neg(x17) , neg(x1) ] ,
+   [ neg(x20) , neg(x16) , pos(x19) ] ,
+   [ pos(x12) , pos(x10) , neg(x11) ] ,
+   [ pos(x6) , neg(x7) , neg(x2) ] ,
+   [ pos(x13) , neg(x10) , pos(x17) ] ,
+   [ neg(x20) , pos(x8) , neg(x16) ] ,
+   [ neg(x10) , neg(x1) , neg(x8) ] ,
+   [ neg(x7) , neg(x3) , pos(x19) ] ,
+   [ pos(x19) , neg(x1) , neg(x6) ] ,
+   [ pos(x19) , neg(x2) , pos(x13) ] ,
+   [ neg(x2) , pos(x20) , neg(x9) ] ,
+   [ neg(x8) , neg(x20) , pos(x16) ] ,
+   [ neg(x13) , neg(x1) , pos(x11) ] ,
+   [ pos(x15) , neg(x12) , neg(x6) ] ,
+   [ neg(x17) , neg(x19) , pos(x9) ] ,
+   [ pos(x19) , neg(x18) , pos(x16) ] ,
+   [ pos(x7) , neg(x8) , neg(x19) ] ,
+   [ neg(x3) , neg(x7) , neg(x1) ] ,
+   [ pos(x7) , neg(x17) , neg(x16) ] ,
+   [ neg(x2) , neg(x14) , pos(x1) ] ,
+   [ neg(x18) , neg(x10) , neg(x8) ] ,
+   [ neg(x16) , pos(x5) , pos(x8) ] ,
+   [ pos(x4) , pos(x8) , pos(x10) ] ,
+   [ neg(x20) , neg(x11) , neg(x19) ] ,
+   [ pos(x8) , neg(x16) , neg(x6) ] ,
+   [ pos(x18) , pos(x12) , pos(x8) ] ,
+   [ neg(x5) , neg(x20) , neg(x10) ] ,
+   [ pos(x16) , pos(x17) , pos(x3) ] ,
+   [ pos(x7) , neg(x1) , neg(x17) ] ,
+   [ pos(x17) , neg(x4) , pos(x7) ] ,
+   [ pos(x20) , neg(x9) , neg(x13) ] ,
+   [ pos(x13) , pos(x18) , pos(x16) ] ,
+   [ neg(x16) , neg(x6) , pos(x5) ] ,
+   [ pos(x5) , pos(x17) , pos(x7) ] ,
+   [ neg(x12) , neg(x17) , neg(x6) ] ,
+   [ neg(x20) , pos(x19) , neg(x5) ] ,
+   [ pos(x9) , neg(x19) , pos(x16) ] ,
+   [ neg(x13) , neg(x16) , pos(x11) ] ,
+   [ neg(x4) , neg(x19) , neg(x18) ] ,
+   [ neg(x13) , pos(x10) , neg(x15) ] ,
+   [ pos(x16) , neg(x7) , neg(x14) ] ,
+   [ neg(x19) , neg(x7) , neg(x18) ] ,
+   [ neg(x20) , pos(x5) , pos(x13) ] ,
+   [ pos(x12) , neg(x6) , pos(x4) ] ,
+   [ pos(x7) , pos(x9) , neg(x13) ] ,
+   [ pos(x16) , pos(x3) , pos(x7) ] ,
+   [ pos(x9) , neg(x1) , pos(x12) ] ,
+   [ neg(x3) , pos(x14) , pos(x7) ] ,
+   [ pos(x1) , pos(x15) , pos(x14) ] ,
+   [ neg(x8) , neg(x11) , pos(x18) ] ,
+   [ pos(x19) , neg(x9) , pos(x7) ] ,
+   [ neg(x10) , pos(x6) , pos(x2) ] ,
+   [ pos(x14) , pos(x18) , neg(x11) ] ,
+   [ neg(x9) , neg(x16) , pos(x14) ] ,
+   [ pos(x1) , pos(x11) , neg(x20) ] ,
+   [ pos(x11) , pos(x12) , neg(x4) ] ,
+   [ pos(x13) , neg(x11) , neg(x14) ] ,
+   [ pos(x17) , neg(x12) , pos(x9) ] ,
+   [ pos(x14) , pos(x9) , pos(x1) ] ,
+   [ pos(x8) , pos(x19) , pos(x4) ] ,
+   [ pos(x6) , neg(x13) , neg(x20) ] ,
+   [ neg(x2) , neg(x13) , pos(x11) ] ,
+   [ pos(x14) , neg(x13) , pos(x17) ] ,
+   [ pos(x9) , neg(x11) , pos(x18) ] ,
+   [ neg(x13) , neg(x6) , pos(x5) ] ,
+   [ pos(x5) , pos(x19) , neg(x18) ] ,
+   [ neg(x4) , pos(x10) , pos(x11) ] ,
+   [ neg(x18) , neg(x19) , neg(x20) ] ,
+   [ pos(x3) , neg(x9) , pos(x8) ]
+   ]).
+problem(5,'schaltung_a1.pl',
+  [
+%a. not_b. c. not_d. e.
+    [pos(a)], [neg(b)], [pos(c)], [neg(d)], [pos(e)],
+% Schaltungen der ersten Ebene
+%and11 :- a,b.
+     [pos(and11),neg(a),neg(b)],
+%or11 :- b.
+     [pos(or11),neg(b)],
+%or11 :- c.
+     [pos(or11),neg(b)],
+%and12 :- c,d.
+     [pos(and12),neg(c),neg(d)],
+%not1 :- not_e.
+     [pos(not1),pos(e)],
+% Schaltungen der zweiten Ebene
+%or21 :- and11.
+     [pos(or21),neg(and11)],
+%or21 :- not1.
+     [pos(or21),neg(not1)],
+%and2 :- or11, not1.
+     [pos(and2),neg(or11),neg(not1)],
+%or22 :- and12.
+     [pos(or22),neg(and12)],
+%or22 :- not1.
+     [pos(or22),neg(not1)],
+%not2 :- e.  % \+ not1.
+     [pos(not2),neg(e)],
+% Schaltungen der dritten Ebene
+%and3 :- or21, and2.
+     [pos(and3),neg(or21),neg(and2)],
+%or3 :- or22.
+     [pos(or3),neg(or22)],
+%or3 :- not2.
+     [pos(or3),neg(not2)],
+% Schaltungen der vierten Ebene
+%or4 :- and3.
+     [pos(or4),neg(and3)],
+%or4 :- or3.
+     [pos(or4),neg(or3)],
+%and4 :- or3, not2.
+     [pos(and4),neg(or3),neg(not2)],
+% Letzte Ebene
+%and5 :- and4, or4.
+     [pos(and5),neg(and4),neg(or4)],
+%output :- and5.
+     [pos(output),neg(and5)],
+% ?- output.
+     [neg(output)]
+   ]).
+
+problem(6, 'doodle-wo-max1-constraint',
+ [
+   [pos(x1),pos(x3)],
+   [neg(x3)],
+   [neg(x5)],
+   [pos(x4),pos(x5)]
+  ]).
+problem(7, 'doodle-with-max1-constraint',
+ [
+   [pos(x1),pos(x3)],
+   [neg(x3)],
+   [neg(x5)],
+   [pos(x4),pos(x5)],
+
+   [neg(x1),neg(x2)], [neg(x1),neg(x3)], [neg(x1),neg(x4)],
+   [neg(x1),neg(x5)],
+   [neg(x2),neg(x3)], [neg(x2),neg(x4)],[neg(x2),neg(x5)],
+   [neg(x3),neg(x4)],[neg(x3),neg(x5)],
+   [neg(x4),neg(x5)]
+  ]).
+```
+
+%% Cell type:code id:c51f1ce6 tags:
+
+``` prolog
+?- test(4).
+```
+
+%% Output
+
+
+
+%% Cell type:code id:bc767ce8 tags:
+
+``` prolog
+```