diff --git a/logic_programming/4_DPLL.ipynb b/logic_programming/4_DPLL.ipynb
index cc310c1069e05c28ef252e074376226e8f679ece..0e698531f720d8fbb46cacb54d3b65a028b846c0 100644
--- a/logic_programming/4_DPLL.ipynb
+++ b/logic_programming/4_DPLL.ipynb
@@ -30,12 +30,14 @@
"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."
+ "Below is an encoding of the CNF as a list of lists.\n",
+ "For example, the clause ```¬A ∨ ¬B ∨ ¬C``` is represented as the list ```[neg(a),neg(b),neg(c)]```.\n",
+ "Every literal is of either the form ```neg(p)``` or ```pos(p)``` with ```p``` being a proposition."
]
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 4,
"id": "964ebd52",
"metadata": {
"vscode": {
@@ -56,6 +58,39 @@
"negate(neg(A),pos(A))."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "a4dc903e",
+ "metadata": {},
+ "source": [
+ "We can negate literals as follows:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "26e0221b",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mNA = neg(a),\n",
+ "NB = pos(b)"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- negate(pos(a),NA), negate(neg(b),NB)."
+ ]
+ },
{
"cell_type": "markdown",
"id": "fc6823ad",
@@ -65,7 +100,8 @@
}
},
"source": [
- "We can pick two clauses and resolve them as follows:"
+ "We now show to perform resolution of two clauses.\n",
+ "First we can pick two clauses simply using ```member```:"
]
},
{
@@ -95,6 +131,14 @@
" member(C1,Clauses), member(Lit1,C1)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "68fd6059",
+ "metadata": {},
+ "source": [
+ "We can now pick matching literals with opposing polarity as follows:"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 5,
@@ -126,9 +170,17 @@
"%comment."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "07785e91",
+ "metadata": {},
+ "source": [
+ "We can now implement resolution of two particular clauses as follows:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 8,
"id": "33fc6271",
"metadata": {
"vscode": {
@@ -144,6 +196,126 @@
" append(R1,R2,Resolvent)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "1d426bb1",
+ "metadata": {},
+ "source": [
+ "The above predicate uses the predicate ```select/3``` from ```library(lists)```, which can be used to select an element from a list and returns a modified list with the element removed:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "f2a8b4a4",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes1 = [1,3]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- select(2,[1,2,3],Res1)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "cba18c66",
+ "metadata": {},
+ "source": [
+ "The predicate ```resolve``` works as follows:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "06aa608c",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mResolvent = [neg(a),pos(c)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- resolve([neg(a),pos(b)],[neg(b),pos(c)],Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "a76d8b5d",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mResolvent = []"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- resolve([pos(b)],[neg(b)],Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "d7a0cc62",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1;31mfalse"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- resolve([neg(a),neg(b)],[neg(b),pos(c)],Resolvent)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "2b2ea192",
+ "metadata": {},
+ "source": [
+ "Let us now resolve two clauses from our puzzle:"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 7,
@@ -173,9 +345,17 @@
" resolve(C1,C2,NewClause)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "a70dbafb",
+ "metadata": {},
+ "source": [
+ "Let us compute all direct resolvents:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 18,
"id": "9d3fbd1a",
"metadata": {
"vscode": {
@@ -187,7 +367,10 @@
"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)]]"
+ "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)]],\n",
+ "NrNew = 22,\n",
+ "SortedC = [[neg(a),neg(a),neg(c)],[neg(a),neg(b),pos(a)],[neg(a),neg(c),neg(a)],[neg(a),neg(c),pos(a)],[neg(a),pos(a)],[neg(b),neg(b),neg(c)],[neg(b),neg(c),neg(b)],[neg(b),neg(c),pos(b)],[neg(b),neg(c),pos(c)],[neg(b),pos(b)],[pos(a),neg(a)],[pos(a),neg(a),neg(b)],[pos(a),neg(a),neg(c)],[pos(a),pos(a)],[pos(b),neg(b)],[pos(b),neg(b),neg(c)],[pos(b),pos(b)],[pos(b),pos(c)],[pos(c),neg(b),neg(c)],[pos(c),pos(b)]],\n",
+ "NrNewUnique = 20"
]
},
"metadata": {},
@@ -197,7 +380,19 @@
"source": [
"?- problem(1,_,Clauses),\n",
" findall(NewClause,(member(C1,Clauses), member(C2,Clauses), \n",
- " resolve(C1,C2,NewClause)), NewClauses)."
+ " resolve(C1,C2,NewClause)\n",
+ " ), NewClauses),\n",
+ " length(NewClauses,NrNew),\n",
+ " sort(NewClauses,SortedC), length(SortedC,NrNewUnique)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "6cdeade5",
+ "metadata": {},
+ "source": [
+ "As you can see, the number of new clauses can grow considerably when applying resolution.\n",
+ "Below we study the DPLL algorithm to check satisfiability of a formula in CNF, using a simple form of resolution (where one clause is a single literal and the other clauses comes from the CNF of the problem)."
]
},
{
@@ -212,12 +407,15 @@
"### DPLL Algorithm\n",
"\n",
"We now present bit by bit the DPLL algorithm as a Prolog program\n",
- "manipulating the above clause database."
+ "manipulating the above clause database.\n",
+ "\n",
+ "The algorithm works by selecting a literal and then making it true and checking whether this leads to a solution.\n",
+ "If not, the algorithm backtracks and makes the negated version of the literal true and tries to find a solution."
]
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 23,
"id": "26924712",
"metadata": {
"vscode": {
@@ -227,7 +425,7 @@
"outputs": [],
"source": [
"becomes_true(TrueLit,Clause) :-\n",
- " member(TrueLit,Clause). "
+ " member(TrueLit,Clause)."
]
},
{
@@ -235,7 +433,7 @@
"id": "17dd1525",
"metadata": {},
"source": [
- "The above checks if making a given literal true makes the second argument, a clause, true:"
+ "The above checks if making a given literal true makes the second argument, a clause, true (i.e., the clause is satisfied):"
]
},
{
@@ -286,9 +484,18 @@
"?- becomes_true(neg(a),[neg(a),pos(b)])."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "62e13b8d",
+ "metadata": {},
+ "source": [
+ "The code below simplifies a clause given a literal ```TrueLit``` that has just become true.\n",
+ "This is done using resolution:"
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 24,
"id": "3b9c87e4",
"metadata": {
"vscode": {
@@ -299,12 +506,20 @@
"source": [
"simplify(TrueLit,Clause,SimplifedClause) :-\n",
" negate(TrueLit,FalseLit),\n",
- " delete(Clause,FalseLit,SimplifedClause). % Resolution with TrueLit\n"
+ " delete(Clause,FalseLit,SimplifedClause). % Resolution with TrueLit if possible\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "e8cee74e",
+ "metadata": {},
+ "source": [
+ "The code uses the ```delete/3``` predicate from ```library(lists)```. Unlike select it also succeeds when the element is not in the list:"
]
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 19,
"id": "0abd90f6",
"metadata": {
"vscode": {
@@ -315,7 +530,7 @@
{
"data": {
"text/plain": [
- "\u001b[1mR = [neg(b),neg(c)]"
+ "\u001b[1mR = [a,b,c]"
]
},
"metadata": {},
@@ -323,7 +538,7 @@
}
],
"source": [
- "?- simplify(pos(a),[neg(a),neg(b),neg(c)],R)."
+ "?- delete([a,b,c],d,R)."
]
},
{
@@ -382,6 +597,14 @@
"?- simplify(pos(c),[pos(a),neg(c)],SC)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "4c3eae55",
+ "metadata": {},
+ "source": [
+ "If no resolution is possible the clause is returned unchanged:"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 16,
@@ -406,9 +629,19 @@
"?- simplify(pos(b),[pos(a),neg(c)],SC)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "441c4145",
+ "metadata": {},
+ "source": [
+ "We can now define the whole procedure to set a literal ```Lit``` to true (```Clauses|{Lit}```) by\n",
+ "- removing all clauses which have become true (and no longer need to be checked)\n",
+ "- simplifying the remaining clauses with resolution if possible."
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 25,
"id": "95fcf64b",
"metadata": {
"vscode": {
@@ -427,13 +660,12 @@
"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."
+ "The predicate ```exclude/3``` from ```library(lists)``` is a higher-order predicate. It maps its first argument (a predicate) over the second argument (a list) and excludes all elements where the predicate succeeds."
]
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 26,
"id": "9c35b0b3",
"metadata": {
"vscode": {
@@ -455,6 +687,56 @@
"?- exclude(becomes_true(pos(a)), [[neg(b)], [pos(a),pos(c)]],R)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "1b1f2fe8",
+ "metadata": {},
+ "source": [
+ "```exclude``` will perform these two calls and hence remove the second clause and keep the first one:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "id": "56175b0d",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1;31mfalse"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mtrue"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- becomes_true(pos(a),[neg(b)]).\n",
+ "?- becomes_true(pos(a),[pos(a),pos(c)])."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "52063b72",
+ "metadata": {},
+ "source": [
+ "The predicate ```maplist/3``` from ```library(lists)``` is another higher-order predicate. It maps its first argument (a predicate) over the elements in the second and third arguments (both lists)."
+ ]
+ },
{
"cell_type": "code",
"execution_count": 19,
@@ -479,6 +761,48 @@
"?- maplist(simplify(neg(c)), [[neg(b),pos(c)], [pos(a),pos(c)]],R)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "44d0ef2e",
+ "metadata": {},
+ "source": [
+ "```maplist``` will perform these two calls and put ```R1``` and ```R2``` into the result list ```R``` above:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "id": "9e0d83d0",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mR1 = [neg(b)],\n",
+ "R2 = [pos(a)]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- simplify(neg(c),[neg(b),pos(c)],R1),\n",
+ " simplify(neg(c),[pos(a),pos(c)],R2)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "007b118b",
+ "metadata": {},
+ "source": [
+ "The predicate ```set_literal``` can now be called as follows:"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 20,
@@ -503,6 +827,71 @@
"?- set_literal(pos(a),[[neg(a),neg(b),neg(c)]],Res)."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "id": "75a52c4f",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = []"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- set_literal(neg(a),[[neg(a),neg(b),neg(c)]],Res)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "04b0de71",
+ "metadata": {},
+ "source": [
+ "In the call above we have found a model: all clauses have been satisfied.\n",
+ "In the next call we have found a contradiction, as the resulting list contains the empty clause (aka the obvious contradiction)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "id": "d8876a92",
+ "metadata": {
+ "vscode": {
+ "languageId": "prolog"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "\u001b[1mRes = [[]]"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "?- set_literal(neg(a),[[neg(a),neg(b),neg(c)],[pos(a)]],Res)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ee321f62",
+ "metadata": {},
+ "source": [
+ "Let us now use this code on our puzzle:"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 21,
@@ -555,9 +944,21 @@
"?- problem(1,_,C1), set_literal(pos(a),C1,C2), set_literal(pos(b),C2,C3)."
]
},
+ {
+ "cell_type": "markdown",
+ "id": "800c4415",
+ "metadata": {},
+ "source": [
+ "This is now the top-level of the DPLL algorithm.\n",
+ "It first tries to find unit clauses, to deterministically find forced assignments.\n",
+ "It then checks if all clauses have now been satisfied.\n",
+ "If not, it checks for inconsistency.\n",
+ "If there is no inconsistency, then a literal is chosen and forced to one and then if required the other value."
+ ]
+ },
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 33,
"id": "b8cabba2",
"metadata": {
"vscode": {
@@ -573,7 +974,7 @@
"dpll([],Stack) :- !, Stack=[]. % SAT\n",
"dpll(Clauses,[branch(Lit)|Stack]) :-\n",
" \\+ member([],Clauses), % no inconsistency\n",
- " choose_literal(Clauses,Lit),\n",
+ " choose_literal(Clauses,Lit), % this selects one literal and returns it first in original then in negated form\n",
" set_literal(Lit,Clauses,Clauses2),\n",
" dpll(Clauses2,Stack). \n",
"\n",
@@ -584,7 +985,7 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 34,
"id": "e369355c",
"metadata": {
"vscode": {
@@ -609,7 +1010,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 35,
"id": "78764141",
"metadata": {
"vscode": {