diff --git a/logic_programming/4_DPLL.ipynb b/logic_programming/4_DPLL.ipynb
index 8b7a211f23e885af4140058547729fee4fb0b67c..cc310c1069e05c28ef252e074376226e8f679ece 100644
--- a/logic_programming/4_DPLL.ipynb
+++ b/logic_programming/4_DPLL.ipynb
@@ -9,23 +9,33 @@
}
},
"source": [
- "We can convert our Knights and Knaves puzzle to conjunctive normal form\n",
+ "# DPLL SAT Solving as a Prolog program\n",
+ "\n",
+ "We take again our Knights and Knaves puzzle from Raymond Smullyan.\n",
+ "\n",
+ "- A says: “B is a knave or C is a knave”\n",
+ "- B says: “A is a knight”\n",
+ "\n",
+ "We can convert our Knights and Knaves puzzle to conjunctive normal form (CNF):\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",
+ "(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."
+ "One can encode a clause as a set of literals, and one can encode the CNF as a set of clauses.\n",
+ "Implicitly, the literals in clause are disjoined, while all the clauses in a CNF are conjoined.\n",
+ "In Prolog, we can represent sets using lists.\n",
+ "Below is an encoding of the CNF as a list of lists."
]
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 3,
"id": "964ebd52",
"metadata": {
"vscode": {
@@ -60,7 +70,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 4,
"id": "152289b6",
"metadata": {
"vscode": {
@@ -87,7 +97,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 5,
"id": "2c3dd1bf",
"metadata": {
"vscode": {
@@ -118,7 +128,7 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 6,
"id": "33fc6271",
"metadata": {
"vscode": {
@@ -136,7 +146,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 7,
"id": "78163b60",
"metadata": {
"vscode": {
@@ -165,7 +175,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 8,
"id": "9d3fbd1a",
"metadata": {
"vscode": {
@@ -207,7 +217,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 9,
"id": "26924712",
"metadata": {
"vscode": {
@@ -230,7 +240,7 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 10,
"id": "7d90c4ad",
"metadata": {
"vscode": {
@@ -254,7 +264,7 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 11,
"id": "d4b4e71f",
"metadata": {
"vscode": {
@@ -278,7 +288,7 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 12,
"id": "3b9c87e4",
"metadata": {
"vscode": {
@@ -294,7 +304,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 13,
"id": "0abd90f6",
"metadata": {
"vscode": {
@@ -318,7 +328,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 14,
"id": "cc81b404",
"metadata": {
"vscode": {
@@ -350,7 +360,7 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 15,
"id": "57df05f0",
"metadata": {
"vscode": {
@@ -374,7 +384,7 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 16,
"id": "a36a54a4",
"metadata": {
"vscode": {
@@ -398,7 +408,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 17,
"id": "95fcf64b",
"metadata": {
"vscode": {
@@ -423,7 +433,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 18,
"id": "9c35b0b3",
"metadata": {
"vscode": {
@@ -447,7 +457,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 19,
"id": "8259d2d7",
"metadata": {
"vscode": {
@@ -471,7 +481,7 @@
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 20,
"id": "25b19d82",
"metadata": {
"vscode": {
@@ -495,7 +505,7 @@
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 21,
"id": "5535384f",
"metadata": {
"vscode": {
@@ -521,7 +531,7 @@
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 22,
"id": "592fcdd9",
"metadata": {
"vscode": {
@@ -547,7 +557,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 23,
"id": "b8cabba2",
"metadata": {
"vscode": {
@@ -574,7 +584,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 24,
"id": "e369355c",
"metadata": {
"vscode": {
@@ -599,7 +609,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 25,
"id": "78764141",
"metadata": {
"vscode": {
@@ -618,7 +628,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 26,
"id": "c51455cf",
"metadata": {
"vscode": {
@@ -652,7 +662,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 27,
"id": "b0466a5d",
"metadata": {
"vscode": {
@@ -683,7 +693,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 28,
"id": "2df16148",
"metadata": {
"vscode": {
@@ -717,7 +727,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 29,
"id": "8d8cf76a",
"metadata": {
"vscode": {
@@ -751,7 +761,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 30,
"id": "31d1b945",
"metadata": {
"vscode": {
@@ -928,7 +938,7 @@
},
{
"cell_type": "code",
- "execution_count": 38,
+ "execution_count": 31,
"id": "c51f1ce6",
"metadata": {
"vscode": {
@@ -962,15 +972,103 @@
},
{
"cell_type": "code",
- "execution_count": null,
- "id": "bc767ce8",
+ "execution_count": 33,
+ "id": "39bb01e4",
"metadata": {
"vscode": {
"languageId": "prolog"
}
},
- "outputs": [],
+ "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": "markdown",
+ "id": "d3ec741b",
+ "metadata": {},
"source": []
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "062d6089",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Version 0.8.0-nightly of Jupyter-Prolog-Kernel"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "jupyter:version."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "03d3fe70",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mA = 0,\n",
+ "B = 8,\n",
+ "C = 0,\n",
+ "D = nightly"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "jupyter:version(A,B,C,D)"
+ ]
}
],
"metadata": {