{ "cells": [ { "cell_type": "markdown", "id": "9eb5530a", "metadata": { "vscode": { "languageId": "prolog" } }, "source": [ "# 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", "```\n", "\n", "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.\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": 4, "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": "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", "metadata": { "vscode": { "languageId": "prolog" } }, "source": [ "We now show to perform resolution of two clauses.\n", "First we can pick two clauses simply using ```member```:" ] }, { "cell_type": "code", "execution_count": 4, "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": "markdown", "id": "68fd6059", "metadata": {}, "source": [ "We can now pick matching literals with opposing polarity as follows:" ] }, { "cell_type": "code", "execution_count": 5, "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": "markdown", "id": "07785e91", "metadata": {}, "source": [ "We can now implement resolution of two particular clauses as follows:" ] }, { "cell_type": "code", "execution_count": 8, "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": "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, "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": "markdown", "id": "a70dbafb", "metadata": {}, "source": [ "Let us compute all direct resolvents:" ] }, { "cell_type": "code", "execution_count": 18, "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)]],\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": {}, "output_type": "display_data" } ], "source": [ "?- problem(1,_,Clauses),\n", " findall(NewClause,(member(C1,Clauses), member(C2,Clauses), \n", " 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)." ] }, { "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.\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": 23, "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 (i.e., the clause is satisfied):" ] }, { "cell_type": "code", "execution_count": 10, "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": 11, "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": "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": 24, "id": "3b9c87e4", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [], "source": [ "simplify(TrueLit,Clause,SimplifedClause) :-\n", " negate(TrueLit,FalseLit),\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": 19, "id": "0abd90f6", "metadata": { "vscode": { "languageId": "prolog" } }, "outputs": [ { "data": { "text/plain": [ "\u001b[1mR = [a,b,c]" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "?- delete([a,b,c],d,R)." ] }, { "cell_type": "code", "execution_count": 14, "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": 15, "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": "markdown", "id": "4c3eae55", "metadata": {}, "source": [ "If no resolution is possible the clause is returned unchanged:" ] }, { "cell_type": "code", "execution_count": 16, "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": "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": 25, "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 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": 26, "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": "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, "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": "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, "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": 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, "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": 22, "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": "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": 33, "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), % 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", "choose_literal([ [Lit|_] | _], Lit).\n", "choose_literal([ [Lit|_] | _], NegLit) :-\n", " negate(Lit,NegLit).\n" ] }, { "cell_type": "code", "execution_count": 34, "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": 35, "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": 26, "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": 27, "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": 28, "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": 29, "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": 30, "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": 31, "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": 33, "id": "39bb01e4", "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": "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": { "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 }